Loogle!

Result

Found 2775 definitions mentioning HMul.hMul and HPow.hPow. Of these, 1282 match your pattern(s). Of these, only the first 200 are shown.

• Nat.shiftLeft_eq Init.Data.Nat.Bitwise.Basic
  ∀ (a b : ℕ), a <<< b = a * 2 ^ b
• Nat.pow_succ' Init.Data.Nat.Lemmas
  ∀ {m n : ℕ}, m ^ n.succ = m * m ^ n
• Nat.pow_add_one' Init.Data.Nat.Lemmas
  ∀ {m n : ℕ}, m ^ (n + 1) = m * m ^ n
• Nat.mul_pow Init.Data.Nat.Lemmas
  ∀ (a b n : ℕ), (a * b) ^ n = a ^ n * b ^ n
• Nat.pow_add Init.Data.Nat.Lemmas
  ∀ (a m n : ℕ), a ^ (m + n) = a ^ m * a ^ n
• Nat.pow_add' Init.Data.Nat.Lemmas
  ∀ (a m n : ℕ), a ^ (m + n) = a ^ n * a ^ m
• Nat.pow_sub_mul_pow Init.Data.Nat.Lemmas
  ∀ (a : ℕ) {m n : ℕ}, m ≤ n → a ^ (n - m) * a ^ m = a ^ n
• Int.pow_succ' Init.Data.Int.Pow
  ∀ (b : ℤ) (e : ℕ), b ^ (e + 1) = b * b ^ e
• Rat.ofScientific_false_def Batteries.Data.Rat.Lemmas
  ∀ {m e : ℕ}, Rat.ofScientific m false e = ↑(m * 10 ^ e)
• Rat.ofScientific_def Batteries.Data.Rat.Lemmas
  ∀ {m : ℕ} {s : Bool} {e : ℕ}, Rat.ofScientific m s e = if s = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)
• pow_mul_comm' Mathlib.Algebra.Group.Defs
  ∀ {M : Type u_2} [inst : Monoid M] (a : M) (n : ℕ), a ^ n * a = a * a ^ n
• pow_succ' Mathlib.Algebra.Group.Defs
  ∀ {M : Type u_2} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ n
• pow_add Mathlib.Algebra.Group.Defs
  ∀ {M : Type u_2} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n
• pow_mul_comm Mathlib.Algebra.Group.Defs
  ∀ {M : Type u_2} [inst : Monoid M] (a : M) (m n : ℕ), a ^ m * a ^ n = a ^ n * a ^ m
• Commute.mul_pow Mathlib.Algebra.Group.Commute.Defs
  ∀ {M : Type u_2} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), (a * b) ^ n = a ^ n * b ^ n
• Commute.mul_zpow Mathlib.Algebra.Group.Commute.Defs
  ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute a b → ∀ (n : ℤ), (a * b) ^ n = a ^ n * b ^ n
• Nat.mul_lt_mul_pow_succ Mathlib.Data.Nat.Defs
  ∀ {a b n : ℕ}, 0 < a → 1 < b → n * b < a * b ^ (n + 1)
• mul_pow_sub_one Mathlib.Algebra.Group.Basic
  ∀ {M : Type u_4} [inst : Monoid M] {n : ℕ}, n ≠ 0 → ∀ (a : M), a * a ^ (n - 1) = a ^ n
• mul_self_zpow Mathlib.Algebra.Group.Basic
  ∀ {G : Type u_3} [inst : Group G] (a : G) (n : ℤ), a * a ^ n = a ^ (n + 1)
• zpow_one_add Mathlib.Algebra.Group.Basic
  ∀ {G : Type u_3} [inst : Group G] (a : G) (n : ℤ), a ^ (1 + n) = a * a ^ n
• pow_mul_pow_sub Mathlib.Algebra.Group.Basic
  ∀ {M : Type u_4} [inst : Monoid M] {m n : ℕ} (a : M), m ≤ n → a ^ m * a ^ (n - m) = a ^ n
• pow_sub_mul_pow Mathlib.Algebra.Group.Basic
  ∀ {M : Type u_4} [inst : Monoid M] {m n : ℕ} (a : M), m ≤ n → a ^ (n - m) * a ^ m = a ^ n
• zpow_add Mathlib.Algebra.Group.Basic
  ∀ {G : Type u_3} [inst : Group G] (a : G) (m n : ℤ), a ^ (m + n) = a ^ m * a ^ n
• pow_mul_pow_eq_one Mathlib.Algebra.Group.Basic
  ∀ {M : Type u_4} [inst : Monoid M] {a b : M} (n : ℕ), a * b = 1 → a ^ n * b ^ n = 1
• mul_pow Mathlib.Algebra.Group.Basic
  ∀ {M : Type u_4} [inst : CommMonoid M] (a b : M) (n : ℕ), (a * b) ^ n = a ^ n * b ^ n
• mul_zpow Mathlib.Algebra.Group.Basic
  ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α) (n : ℤ), (a * b) ^ n = a ^ n * b ^ n
• zpow_mul_comm Mathlib.Algebra.Group.Basic
  ∀ {G : Type u_3} [inst : Group G] (a : G) (m n : ℤ), a ^ m * a ^ n = a ^ n * a ^ m
• mul_zpow_neg_one Mathlib.Algebra.Group.Basic
  ∀ {α : Type u_1} [inst : DivisionMonoid α] (a b : α), (a * b) ^ (-1) = b ^ (-1) * a ^ (-1)
• inv_pow_sub Mathlib.Algebra.Group.Basic
  ∀ {G : Type u_3} [inst : Group G] (a : G) {m n : ℕ}, n ≤ m → a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
• mul_right_iterate Mathlib.Algebra.GroupPower.IterateHom
  ∀ {G : Type u_3} [inst : Monoid G] (a : G) (n : ℕ), (fun x => x * a)^[n] = fun x => x * a ^ n
• zpow_one_add₀ Mathlib.Algebra.GroupWithZero.Basic
  ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (i : ℤ), a ^ (1 + i) = a * a ^ i
• zpow_add₀ Mathlib.Algebra.GroupWithZero.Basic
  ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (m n : ℤ), a ^ (m + n) = a ^ m * a ^ n
• zpow_add' Mathlib.Algebra.GroupWithZero.Basic
  ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a : G₀} {m n : ℤ}, a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0 → a ^ (m + n) = a ^ m * a ^ n
• zpow_neg_mul_zpow_self Mathlib.Algebra.GroupWithZero.Units.Basic
  ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} (n : ℤ), a ≠ 0 → a ^ (-n) * a ^ n = 1
• inv_pow_sub_of_lt Mathlib.Algebra.GroupWithZero.Units.Basic
  ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {m n : ℕ} (a : G₀), n < m → a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
• inv_pow_sub₀ Mathlib.Algebra.GroupWithZero.Units.Basic
  ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} {m n : ℕ}, a ≠ 0 → n ≤ m → a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
• Units.conj_pow Mathlib.Algebra.Group.Semiconj.Units
  ∀ {M : Type u_1} [inst : Monoid M] (u : Mˣ) (x : M) (n : ℕ), (↑u * x * ↑u⁻¹) ^ n = ↑u * x ^ n * ↑u⁻¹
• Units.conj_pow' Mathlib.Algebra.Group.Semiconj.Units
  ∀ {M : Type u_1} [inst : Monoid M] (u : Mˣ) (x : M) (n : ℕ), (↑u⁻¹ * x * ↑u) ^ n = ↑u⁻¹ * x ^ n * ↑u
• pow_inv_comm₀ Mathlib.Algebra.GroupWithZero.Commute
  ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] (a : G₀) (m n : ℕ), a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m
• mul_neg_one_pow_eq_zero_iff Mathlib.Algebra.Ring.Commute
  ∀ {R : Type u} [inst : Ring R] {a : R} {n : ℕ}, a * (-1) ^ n = 0 ↔ a = 0
• neg_pow Mathlib.Algebra.Ring.Commute
  ∀ {R : Type u} [inst : Monoid R] [inst_1 : HasDistribNeg R] (a : R) (n : ℕ), (-a) ^ n = (-1) ^ n * a ^ n
• neg_pow' Mathlib.Algebra.Ring.Commute
  ∀ {R : Type u} [inst : Monoid R] [inst_1 : HasDistribNeg R] (a : R) (n : ℕ), (-a) ^ n = a ^ n * (-1) ^ n
• sign_cases_of_C_mul_pow_nonneg Mathlib.Algebra.Order.Ring.Unbundled.Basic
  ∀ {α : Type u} [inst : Semiring α] [inst_1 : LinearOrder α] {a b : α} [inst_2 : PosMulStrictMono α], (∀ (n : ℕ), 0 ≤ a * b ^ n) → a = 0 ∨ 0 < a ∧ 0 ≤ b
• Nat.two_mul_sq_add_one_le_two_pow_two_mul Mathlib.Data.Nat.Cast.Order.Ring
  ∀ (k : ℕ), 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
• Set.pairwise_disjoint_Ico_mul_zpow Mathlib.Algebra.Order.Interval.Set.Group
  ∀ {α : Type u_1} [inst : OrderedCommGroup α] (a b : α), Pairwise (Disjoint on fun n => Set.Ico (a * b ^ n) (a * b ^ (n + 1)))
• Set.pairwise_disjoint_Ioc_mul_zpow Mathlib.Algebra.Order.Interval.Set.Group
  ∀ {α : Type u_1} [inst : OrderedCommGroup α] (a b : α), Pairwise (Disjoint on fun n => Set.Ioc (a * b ^ n) (a * b ^ (n + 1)))
• Set.pairwise_disjoint_Ioo_mul_zpow Mathlib.Algebra.Order.Interval.Set.Group
  ∀ {α : Type u_1} [inst : OrderedCommGroup α] (a b : α), Pairwise (Disjoint on fun n => Set.Ioo (a * b ^ n) (a * b ^ (n + 1)))
• Nat.and_two_pow Mathlib.Data.Nat.Bitwise
  ∀ (n i : ℕ), n &&& 2 ^ i = (n.testBit i).toNat * 2 ^ i
• Nat.shiftLeft_eq_mul_pow Mathlib.Data.Nat.Size
  ∀ (m n : ℕ), m <<< n = m * 2 ^ n
• Nat.shiftLeft'_tt_eq_mul_pow Mathlib.Data.Nat.Size
  ∀ (m n : ℕ), Nat.shiftLeft' true m n + 1 = (m + 1) * 2 ^ n
• pow_add_pow_le' Mathlib.Algebra.Order.Ring.Basic
  ∀ {R : Type u_3} [inst : OrderedSemiring R] {a b : R} {n : ℕ}, 0 ≤ a → 0 ≤ b → a ^ n + b ^ n ≤ 2 * (a + b) ^ n
• Rat.ofScientific.eq_1 Mathlib.Algebra.Order.Ring.Unbundled.Rat
  ∀ (m : ℕ) (s : Bool) (e : ℕ), Rat.ofScientific m s e = if s = true then Rat.normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)
• pow_inv_comm Mathlib.Algebra.Group.Commute.Basic
  ∀ {G : Type u_1} [inst : Group G] (a : G) (m n : ℕ), a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m
• CancelDenoms.pow_subst Mathlib.Tactic.CancelDenoms.Core
  ∀ {α : Type u_1} [inst : CommRing α] {n e1 t1 k l : α} {e2 : ℕ}, n * e1 = t1 → l * n ^ e2 = k → k * e1 ^ e2 = l * t1 ^ e2
• Nat.factorial_mul_pow_sub_le_factorial Mathlib.Data.Nat.Factorial.Basic
  ∀ {n m : ℕ}, n ≤ m → n.factorial * n ^ (m - n) ≤ m.factorial
• Nat.factorial_mul_pow_le_factorial Mathlib.Data.Nat.Factorial.Basic
  ∀ {m n : ℕ}, m.factorial * (m + 1) ^ n ≤ (m + n).factorial
• existsUnique_add_zpow_mem_Ioc Mathlib.Algebra.Order.Archimedean.Basic
  ∀ {α : Type u_1} [inst : LinearOrderedCommGroup α] [inst_1 : MulArchimedean α] {a : α}, 1 < a → ∀ (b c : α), ∃! m, b * a ^ m ∈ Set.Ioc c (c * a)
• existsUnique_mul_zpow_mem_Ico Mathlib.Algebra.Order.Archimedean.Basic
  ∀ {α : Type u_1} [inst : LinearOrderedCommGroup α] [inst_1 : MulArchimedean α] {a : α}, 1 < a → ∀ (b c : α), ∃! m, b * a ^ m ∈ Set.Ico c (c * a)
• List.alternatingProd_append Mathlib.Algebra.BigOperators.Group.List
  ∀ {α : Type u_2} [inst : CommGroup α] (l₁ l₂ : List α), (l₁ ++ l₂).alternatingProd = l₁.alternatingProd * l₂.alternatingProd ^ (-1) ^ l₁.length
• Finset.prod_mul_pow_card Mathlib.Algebra.BigOperators.Group.Finset
  ∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [inst : CommMonoid β] {b : β}, (∏ a ∈ s, f a) * b ^ s.card = ∏ a ∈ s, f a * b
• Submonoid.mem_closure_pair Mathlib.Algebra.Group.Submonoid.Membership
  ∀ {A : Type u_4} [inst : CommMonoid A] (a b c : A), c ∈ Submonoid.closure {a, b} ↔ ∃ m n, a ^ m * b ^ n = c
• conj_zpow Mathlib.Algebra.Group.Conj
  ∀ {α : Type u} [inst : Group α] {i : ℤ} {a b : α}, (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
• conj_pow Mathlib.Algebra.Group.Conj
  ∀ {α : Type u} [inst : Group α] {i : ℕ} {a b : α}, (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
• Subgroup.mem_closure_pair Mathlib.Algebra.Group.Subgroup.Basic
  ∀ {C : Type u_6} [inst : CommGroup C] {x y z : C}, z ∈ Subgroup.closure {x, y} ↔ ∃ m n, x ^ m * y ^ n = z
• Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd Mathlib.Algebra.Associated.Basic
  ∀ {M : Type u_1} [inst : CancelCommMonoidWithZero M] {p a b : M} {n : ℕ}, Prime p → p ^ n.succ ∣ a ^ n.succ * b ^ n → ¬p ^ 2 ∣ b → p ∣ a
• Algebra.mul_sub_algebraMap_pow_commutes Mathlib.Algebra.Algebra.Basic
  ∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] (x : A) (r : R) (n : ℕ), x * (x - (algebraMap R A) r) ^ n = (x - (algebraMap R A) r) ^ n * x
• Finset.sum_pow_mul_eq_add_pow Mathlib.Algebra.BigOperators.Ring
  ∀ {ι : Type u_1} {α : Type u_3} [inst : CommSemiring α] (a b : α) (s : Finset ι), ∑ t ∈ s.powerset, a ^ t.card * b ^ (s.card - t.card) = (a + b) ^ s.card
• Fintype.sum_pow_mul_eq_add_pow Mathlib.Algebra.BigOperators.Ring
  ∀ {α : Type u_3} [inst : CommSemiring α] (ι : Type u_7) [inst_1 : Fintype ι] (a b : α), ∑ s : Finset ι, a ^ s.card * b ^ (Fintype.card ι - s.card) = (a + b) ^ Fintype.card ι
• finFunctionFinEquiv_apply Mathlib.Algebra.BigOperators.Fin
  ∀ {m n : ℕ} (f : Fin n → Fin m), ↑(finFunctionFinEquiv f) = ∑ i : Fin n, ↑(f i) * m ^ ↑i
• finFunctionFinEquiv_apply_val Mathlib.Algebra.BigOperators.Fin
  ∀ {m n : ℕ} (f : Fin n → Fin m), ↑(finFunctionFinEquiv f) = ∑ i : Fin n, ↑(f i) * m ^ ↑i
• finFunctionFinEquiv_single Mathlib.Algebra.BigOperators.Fin
  ∀ {m n : ℕ} [inst : NeZero m] (i : Fin n) (j : Fin m), ↑(finFunctionFinEquiv (Pi.single i j)) = ↑j * m ^ ↑i
• Fin.sum_pow_mul_eq_add_pow Mathlib.Algebra.BigOperators.Fin
  ∀ {n : ℕ} {R : Type u_3} [inst : CommSemiring R] (a b : R), ∑ s : Finset (Fin n), a ^ s.card * b ^ (n - s.card) = (a + b) ^ n
• Commute.add_pow' Mathlib.Data.Nat.Choose.Sum
  ∀ {R : Type u_1} [inst : Semiring R] {x y : R}, Commute x y → ∀ (n : ℕ), (x + y) ^ n = ∑ m ∈ Finset.antidiagonal n, n.choose m.1 • (x ^ m.1 * y ^ m.2)
• Commute.add_pow Mathlib.Data.Nat.Choose.Sum
  ∀ {R : Type u_1} [inst : Semiring R] {x y : R}, Commute x y → ∀ (n : ℕ), (x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)
• add_pow Mathlib.Data.Nat.Choose.Sum
  ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) (n : ℕ), (x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)
• sub_pow Mathlib.Data.Nat.Choose.Sum
  ∀ {R : Type u_1} [inst : CommRing R] (x y : R) (n : ℕ), (x - y) ^ n = ∑ m ∈ Finset.range (n + 1), (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)
• Submodule.pow_induction_on_left' Mathlib.Algebra.Algebra.Operations
  ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M : Submodule R A) {C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop}, (∀ (r : R), C 0 ((algebraMap R A) r) ⋯) → (∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯) → (∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯) → ∀ {n : ℕ} {x : A} (hx : x ∈ M ^ n), C n x hx
• Cardinal.mul_power Mathlib.SetTheory.Cardinal.Basic
  ∀ {a b c : Cardinal.{u_1}}, (a * b) ^ c = a ^ c * b ^ c
• Cardinal.power_add Mathlib.SetTheory.Cardinal.Basic
  ∀ (a b c : Cardinal.{u_1}), a ^ (b + c) = a ^ b * a ^ c
• Ordinal.opow_one_add Mathlib.SetTheory.Ordinal.Exponential
  ∀ (a b : Ordinal.{u_1}), a ^ (1 + b) = a * a ^ b
• Ordinal.opow_add Mathlib.SetTheory.Ordinal.Exponential
  ∀ (a b c : Ordinal.{u_1}), a ^ (b + c) = a ^ b * a ^ c
• Ordinal.mul_omega0_opow_opow Mathlib.SetTheory.Ordinal.Principal
  ∀ {a b : Ordinal.{u_1}}, 0 < a → a < Ordinal.omega0 ^ Ordinal.omega0 ^ b → a * Ordinal.omega0 ^ Ordinal.omega0 ^ b = Ordinal.omega0 ^ Ordinal.omega0 ^ b
• Ordinal.mul_omega_opow_opow Mathlib.SetTheory.Ordinal.Principal
  ∀ {a b : Ordinal.{u_1}}, 0 < a → a < Ordinal.omega0 ^ Ordinal.omega0 ^ b → a * Ordinal.omega0 ^ Ordinal.omega0 ^ b = Ordinal.omega0 ^ Ordinal.omega0 ^ b
• Nat.exists_mul_pow_lt_factorial Mathlib.Order.Filter.AtTopBot
  ∀ (a c : ℕ), ∃ n0, ∀ n ≥ n0, a * c ^ n < (n - 1).factorial
• Nat.eventually_mul_pow_lt_factorial_sub Mathlib.Order.Filter.AtTopBot
  ∀ (a c d : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, a * c ^ n < (n - d).factorial
• Mathlib.Tactic.Group.zpow_trick_one Mathlib.Tactic.Group
  ∀ {G : Type u_1} [inst : Group G] (a b : G) (m : ℤ), a * b * b ^ m = a * b ^ (m + 1)
• Mathlib.Tactic.Group.zpow_trick_one' Mathlib.Tactic.Group
  ∀ {G : Type u_1} [inst : Group G] (a b : G) (n : ℤ), a * b ^ n * b = a * b ^ (n + 1)
• Mathlib.Tactic.Group.zpow_trick Mathlib.Tactic.Group
  ∀ {G : Type u_1} [inst : Group G] (a b : G) (n m : ℤ), a * b ^ n * b ^ m = a * b ^ (n + m)
• QuotientGroup.out'_conj_pow_minimalPeriod_mem Mathlib.GroupTheory.GroupAction.Quotient
  ∀ {α : Type u} [inst : Group α] (H : Subgroup α) (a : α) (q : α ⧸ H), (Quotient.out' q)⁻¹ * a ^ Function.minimalPeriod (fun x => a • x) q * Quotient.out' q ∈ H
• npow_add Mathlib.Algebra.Group.NatPowAssoc
  ∀ {M : Type u_1} [inst : MulOneClass M] [inst_1 : Pow M ℕ] [inst_2 : NatPowAssoc M] (k n : ℕ) (x : M), x ^ (k + n) = x ^ k * x ^ n
• NatPowAssoc.npow_add Mathlib.Algebra.Group.NatPowAssoc
  ∀ {M : Type u_2} {inst : MulOneClass M} {inst_1 : Pow M ℕ} [self : NatPowAssoc M] (k n : ℕ) (x : M), x ^ (k + n) = x ^ k * x ^ n
• npow_mul_comm Mathlib.Algebra.Group.NatPowAssoc
  ∀ {M : Type u_1} [inst : MulOneClass M] [inst_1 : Pow M ℕ] [inst_2 : NatPowAssoc M] (m n : ℕ) (x : M), x ^ m * x ^ n = x ^ n * x ^ m
• NatPowAssoc.mk Mathlib.Algebra.Group.NatPowAssoc
  ∀ {M : Type u_2} [inst : MulOneClass M] [inst_1 : Pow M ℕ], (∀ (k n : ℕ) (x : M), x ^ (k + n) = x ^ k * x ^ n) → (∀ (x : M), x ^ 0 = 1) → (∀ (x : M), x ^ 1 = x) → NatPowAssoc M
• npow_mul_assoc Mathlib.Algebra.Group.NatPowAssoc
  ∀ {M : Type u_1} [inst : MulOneClass M] [inst_1 : Pow M ℕ] [inst_2 : NatPowAssoc M] (k m n : ℕ) (x : M), x ^ k * x ^ m * x ^ n = x ^ k * (x ^ m * x ^ n)
• geom_sum₂_with_one Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : Semiring α] (x : α) (n : ℕ), ∑ i ∈ Finset.range n, x ^ i * 1 ^ (n - 1 - i) = ∑ i ∈ Finset.range n, x ^ i
• geom_sum₂_self Mathlib.Algebra.GeomSum
  ∀ {α : Type u_1} [inst : CommRing α] (x : α) (n : ℕ), ∑ i ∈ Finset.range n, x ^ i * x ^ (n - 1 - i) = ↑n * x ^ (n - 1)
• Commute.geom_sum₂_mul Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : Ring α] {x y : α}, Commute x y → ∀ (n : ℕ), (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
• Commute.mul_geom_sum₂ Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : Ring α] {x y : α}, Commute x y → ∀ (n : ℕ), (x - y) * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = x ^ n - y ^ n
• Commute.mul_neg_geom_sum₂ Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : Ring α] {x y : α}, Commute x y → ∀ (n : ℕ), (y - x) * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = y ^ n - x ^ n
• Commute.geom_sum₂_comm Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : Semiring α] {x y : α} (n : ℕ), Commute x y → ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ Finset.range n, y ^ i * x ^ (n - 1 - i)
• geom_sum₂_mul Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : CommRing α] (x y : α) (n : ℕ), (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
• geom_sum₂_comm Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : CommSemiring α] (x y : α) (n : ℕ), ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ Finset.range n, y ^ i * x ^ (n - 1 - i)
• Commute.geom_sum₂ Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : DivisionRing α] {x y : α}, Commute x y → x ≠ y → ∀ (n : ℕ), ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
• Commute.geom_sum₂_mul_add Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : Semiring α] {x y : α}, Commute x y → ∀ (n : ℕ), (∑ i ∈ Finset.range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
• geom₂_sum Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : Field α] {x y : α}, x ≠ y → ∀ (n : ℕ), ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
• geom_sum₂_mul_add Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : CommSemiring α] (x y : α) (n : ℕ), (∑ i ∈ Finset.range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
• op_geom_sum₂ Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : Semiring α] (x y : α) (n : ℕ), ∑ i ∈ Finset.range n, MulOpposite.op y ^ (n - 1 - i) * MulOpposite.op x ^ i = ∑ i ∈ Finset.range n, MulOpposite.op y ^ i * MulOpposite.op x ^ (n - 1 - i)
• Commute.geom_sum₂_Ico_mul Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : Ring α] {x y : α}, Commute x y → ∀ {m n : ℕ}, m ≤ n → (∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ (n - m) * x ^ m
• Commute.mul_geom_sum₂_Ico Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : Ring α] {x y : α}, Commute x y → ∀ {m n : ℕ}, m ≤ n → (x - y) * ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)
• mul_geom_sum₂_Ico Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : CommRing α] (x y : α) {m n : ℕ}, m ≤ n → (x - y) * ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)
• Commute.geom_sum₂_succ_eq Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : Ring α] {x y : α}, Commute x y → ∀ {n : ℕ}, ∑ i ∈ Finset.range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)
• RingHom.map_geom_sum₂ Mathlib.Algebra.GeomSum
  ∀ {α : Type u} {β : Type u_1} [inst : Semiring α] [inst_1 : Semiring β] (x y : α) (n : ℕ) (f : α →+* β), f (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) = ∑ i ∈ Finset.range n, f x ^ i * f y ^ (n - 1 - i)
• geom_sum₂_succ_eq Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : CommRing α] (x y : α) {n : ℕ}, ∑ i ∈ Finset.range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)
• Commute.geom_sum₂_Ico Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : DivisionRing α] {x y : α}, Commute x y → x ≠ y → ∀ {m n : ℕ}, m ≤ n → ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
• geom_sum₂_Ico Mathlib.Algebra.GeomSum
  ∀ {α : Type u} [inst : Field α] {x y : α}, x ≠ y → ∀ {m n : ℕ}, m ≤ n → ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
• Nat.ofDigits_eq_sum_mapIdx Mathlib.Data.Nat.Digits
  ∀ (b : ℕ) (L : List ℕ), Nat.ofDigits b L = (List.mapIdx (fun i a => a * b ^ i) L).sum
• Nat.ofDigits_eq_sum_map_with_index_aux Mathlib.Data.Nat.Digits
  ∀ (b : ℕ) (l : List ℕ), (List.zipWith (fun i a => a * b ^ (i + 1)) (List.range l.length) l).sum = b * (List.zipWith (fun i a => a * b ^ i) (List.range l.length) l).sum
• sub_pow_eq_sub_pow_mod_mul_pow_sub_pow_div Mathlib.Algebra.CharP.Basic
  ∀ (R : Type u_1) (x y : R) (n : ℕ) [inst : CommRing R] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP R p], (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
• add_pow_eq_add_pow_mod_mul_pow_add_pow_div Mathlib.Algebra.CharP.Basic
  ∀ (R : Type u_1) (n : ℕ) [inst : CommSemiring R] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP R p] (x y : R), (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
• Commute.add_pow_prime_eq Mathlib.Algebra.CharP.Basic
  ∀ {R : Type u_1} [inst : Semiring R] {p : ℕ}, Nat.Prime p → ∀ {x y : R}, Commute x y → (x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k ∈ Finset.Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)
• add_pow_prime_eq Mathlib.Algebra.CharP.Basic
  ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ}, Nat.Prime p → ∀ (x y : R), (x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k ∈ Finset.Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)
• Commute.add_pow_prime_pow_eq Mathlib.Algebra.CharP.Basic
  ∀ {R : Type u_1} [inst : Semiring R] {p : ℕ}, Nat.Prime p → ∀ {x y : R}, Commute x y → ∀ (n : ℕ), (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Finset.Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)
• add_pow_prime_pow_eq Mathlib.Algebra.CharP.Basic
  ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ}, Nat.Prime p → ∀ (x y : R) (n : ℕ), (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Finset.Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)
• Nat.ord_proj_mul Mathlib.Data.Nat.Factorization.Basic
  ∀ {a b : ℕ} (p : ℕ), a ≠ 0 → b ≠ 0 → p ^ (a * b).factorization p = p ^ a.factorization p * p ^ b.factorization p
• uzpow_add Mathlib.Data.ZMod.IntUnitsPower
  ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : Module R (Additive ℤˣ)] (s : ℤˣ) (x y : R), s ^ (x + y) = s ^ x * s ^ y
• mul_uzpow Mathlib.Data.ZMod.IntUnitsPower
  ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : Module R (Additive ℤˣ)] (s₁ s₂ : ℤˣ) (x : R), (s₁ * s₂) ^ x = s₁ ^ x * s₂ ^ x
• prime_two_or_dvd_of_dvd_two_mul_pow_self_two Mathlib.RingTheory.Int.Basic
  ∀ {m : ℤ} {p : ℕ}, Nat.Prime p → ↑p ∣ 2 * m ^ 2 → p = 2 ∨ p ∣ m.natAbs
• Commute.orderOf_mul_pow_eq_lcm Mathlib.GroupTheory.Exponent
  ∀ {G : Type u} [inst : Monoid G] {x y : G}, Commute x y → orderOf x ≠ 0 → orderOf y ≠ 0 → orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)) * y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) = (orderOf x).lcm (orderOf y)
• MvPolynomial.C_mul_X_pow_eq_monomial Mathlib.Algebra.MvPolynomial.Basic
  ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {s : σ} {a : R} {n : ℕ}, MvPolynomial.C a * MvPolynomial.X s ^ n = (MvPolynomial.monomial fun₀ | s => n) a
• MvPolynomial.monomial_add_single Mathlib.Algebra.MvPolynomial.Basic
  ∀ {R : Type u} {σ : Type u_1} {a : R} {e : ℕ} {n : σ} {s : σ →₀ ℕ} [inst : CommSemiring R], (MvPolynomial.monomial (s + fun₀ | n => e)) a = (MvPolynomial.monomial s) a * MvPolynomial.X n ^ e
• Polynomial.support_C_mul_X_pow' Mathlib.Algebra.Polynomial.Basic
  ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (c : R), (Polynomial.C c * Polynomial.X ^ n).support ⊆ {n}
• Polynomial.X_pow_mul Mathlib.Algebra.Polynomial.Basic
  ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, Polynomial.X ^ n * p = p * Polynomial.X ^ n
• Polynomial.toFinsupp_C_mul_X_pow Mathlib.Algebra.Polynomial.Basic
  ∀ {R : Type u} [inst : Semiring R] (a : R) (n : ℕ), (Polynomial.C a * Polynomial.X ^ n).toFinsupp = fun₀ | n => a
• Polynomial.support_C_mul_X_pow Mathlib.Algebra.Polynomial.Basic
  ∀ {R : Type u} [inst : Semiring R] (n : ℕ) {c : R}, c ≠ 0 → (Polynomial.C c * Polynomial.X ^ n).support = {n}
• Polynomial.sum_C_mul_X_pow_eq Mathlib.Algebra.Polynomial.Basic
  ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), (p.sum fun n a => Polynomial.C a * Polynomial.X ^ n) = p
• Polynomial.X_pow_mul_assoc Mathlib.Algebra.Polynomial.Basic
  ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} {n : ℕ}, p * Polynomial.X ^ n * q = p * q * Polynomial.X ^ n
• Polynomial.X_pow_mul_C Mathlib.Algebra.Polynomial.Basic
  ∀ {R : Type u} [inst : Semiring R] (r : R) (n : ℕ), Polynomial.X ^ n * Polynomial.C r = Polynomial.C r * Polynomial.X ^ n
• Polynomial.C_mul_X_pow_eq_monomial Mathlib.Algebra.Polynomial.Basic
  ∀ {R : Type u} {a : R} [inst : Semiring R] {n : ℕ}, Polynomial.C a * Polynomial.X ^ n = (Polynomial.monomial n) a
• Polynomial.support_binomial' Mathlib.Algebra.Polynomial.Basic
  ∀ {R : Type u} [inst : Semiring R] (k m : ℕ) (x y : R), (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support ⊆ {k, m}
• Polynomial.X_pow_mul_assoc_C Mathlib.Algebra.Polynomial.Basic
  ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ} (r : R), p * Polynomial.X ^ n * Polynomial.C r = p * Polynomial.C r * Polynomial.X ^ n
• Polynomial.monomial_mul_X_pow Mathlib.Algebra.Polynomial.Basic
  ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (r : R) (k : ℕ), (Polynomial.monomial n) r * Polynomial.X ^ k = (Polynomial.monomial (n + k)) r
• Polynomial.support_trinomial' Mathlib.Algebra.Polynomial.Basic
  ∀ {R : Type u} [inst : Semiring R] (k m n : ℕ) (x y z : R), (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support ⊆ {k, m, n}
• Polynomial.binomial_eq_binomial Mathlib.Algebra.Polynomial.Basic
  ∀ {R : Type u} [inst : Semiring R] {k l m n : ℕ} {u v : R}, u ≠ 0 → v ≠ 0 → (Polynomial.C u * Polynomial.X ^ k + Polynomial.C v * Polynomial.X ^ l = Polynomial.C u * Polynomial.X ^ m + Polynomial.C v * Polynomial.X ^ n ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n)
• Polynomial.coeff_mul_X_pow Mathlib.Algebra.Polynomial.Coeff
  ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n d : ℕ), (p * Polynomial.X ^ n).coeff (d + n) = p.coeff d
• Polynomial.mul_X_pow_eq_zero Mathlib.Algebra.Polynomial.Coeff
  ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p * Polynomial.X ^ n = 0 → p = 0
• Polynomial.coeff_mul_X_pow' Mathlib.Algebra.Polynomial.Coeff
  ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n d : ℕ), (p * Polynomial.X ^ n).coeff d = if n ≤ d then p.coeff (d - n) else 0
• Polynomial.coeff_C_mul_X_pow Mathlib.Algebra.Polynomial.Coeff
  ∀ {R : Type u} [inst : Semiring R] (x : R) (k n : ℕ), (Polynomial.C x * Polynomial.X ^ k).coeff n = if n = k then x else 0
• Polynomial.update_eq_add_sub_coeff Mathlib.Algebra.Polynomial.Coeff
  ∀ {R : Type u_1} [inst : Ring R] (p : Polynomial R) (n : ℕ) (a : R), p.update n a = p + Polynomial.C (a - p.coeff n) * Polynomial.X ^ n
• Polynomial.card_support_binomial Mathlib.Algebra.Polynomial.Coeff
  ∀ {R : Type u} [inst : Semiring R] {k m : ℕ}, k ≠ m → ∀ {x y : R}, x ≠ 0 → y ≠ 0 → (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support.card = 2
• Polynomial.support_binomial Mathlib.Algebra.Polynomial.Coeff
  ∀ {R : Type u} [inst : Semiring R] {k m : ℕ}, k ≠ m → ∀ {x y : R}, x ≠ 0 → y ≠ 0 → (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support = {k, m}
• Polynomial.card_support_trinomial Mathlib.Algebra.Polynomial.Coeff
  ∀ {R : Type u} [inst : Semiring R] {k m n : ℕ}, k < m → m < n → ∀ {x y z : R}, x ≠ 0 → y ≠ 0 → z ≠ 0 → (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support.card = 3
• Polynomial.support_trinomial Mathlib.Algebra.Polynomial.Coeff
  ∀ {R : Type u} [inst : Semiring R] {k m n : ℕ}, k < m → m < n → ∀ {x y z : R}, x ≠ 0 → y ≠ 0 → z ≠ 0 → (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support = {k, m, n}
• Polynomial.leadingCoeff_mul_X_pow Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, (p * Polynomial.X ^ n).leadingCoeff = p.leadingCoeff
• Polynomial.natDegree_mul_X_pow Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} [inst : Semiring R] [inst_1 : Nontrivial R] {p : Polynomial R} (n : ℕ), p ≠ 0 → (p * Polynomial.X ^ n).natDegree = p.natDegree + n
• Polynomial.degree_mul_X_pow Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} [inst : Semiring R] [inst_1 : Nontrivial R] {p : Polynomial R} (n : ℕ), (p * Polynomial.X ^ n).degree = p.degree + ↑n
• Polynomial.leadingCoeff_C_mul_X_pow Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} [inst : Semiring R] (a : R) (n : ℕ), (Polynomial.C a * Polynomial.X ^ n).leadingCoeff = a
• Polynomial.natDegree_C_mul_X_pow_le Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} [inst : Semiring R] (a : R) (n : ℕ), (Polynomial.C a * Polynomial.X ^ n).natDegree ≤ n
• Polynomial.card_support_C_mul_X_pow_le_one Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} [inst : Semiring R] {c : R} {n : ℕ}, (Polynomial.C c * Polynomial.X ^ n).support.card ≤ 1
• Polynomial.mem_support_C_mul_X_pow Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} [inst : Semiring R] {n a : ℕ} {c : R}, a ∈ (Polynomial.C c * Polynomial.X ^ n).support → a = n
• Polynomial.natDegree_C_mul_X_pow Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (a : R), a ≠ 0 → (Polynomial.C a * Polynomial.X ^ n).natDegree = n
• Polynomial.C_mul_X_pow_eq_self Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.support.card ≤ 1 → Polynomial.C p.leadingCoeff * Polynomial.X ^ p.natDegree = p
• Polynomial.degree_C_mul_X_pow_le Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (a : R), (Polynomial.C a * Polynomial.X ^ n).degree ≤ ↑n
• Polynomial.as_sum_support_C_mul_X_pow Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p = ∑ i ∈ p.support, Polynomial.C (p.coeff i) * Polynomial.X ^ i
• Polynomial.degree_C_mul_X_pow Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} {a : R} [inst : Semiring R] (n : ℕ), a ≠ 0 → (Polynomial.C a * Polynomial.X ^ n).degree = ↑n
• Polynomial.as_sum_range_C_mul_X_pow Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p = ∑ i ∈ Finset.range (p.natDegree + 1), Polynomial.C (p.coeff i) * Polynomial.X ^ i
• Polynomial.degree_sum_fin_lt Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} [inst : Semiring R] {n : ℕ} (f : Fin n → R), (∑ i : Fin n, Polynomial.C (f i) * Polynomial.X ^ ↑i).degree < ↑n
• Polynomial.natDegree_quadratic_le Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} {a b c : R} [inst : Semiring R], (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).natDegree ≤ 2
• Polynomial.degree_linear_lt_degree_C_mul_X_sq Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} {a b c : R} [inst : Semiring R], a ≠ 0 → (Polynomial.C b * Polynomial.X + Polynomial.C c).degree < (Polynomial.C a * Polynomial.X ^ 2).degree
• Polynomial.leadingCoeff_quadratic Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} {a b c : R} [inst : Semiring R], a ≠ 0 → (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).leadingCoeff = a
• Polynomial.natDegree_quadratic Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} {a b c : R} [inst : Semiring R], a ≠ 0 → (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).natDegree = 2
• Polynomial.degree_quadratic_le Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} {a b c : R} [inst : Semiring R], (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree ≤ 2
• Polynomial.degree_quadratic_lt Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} {a b c : R} [inst : Semiring R], (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree < 3
• Polynomial.degree_quadratic Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} {a b c : R} [inst : Semiring R], a ≠ 0 → (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree = 2
• Polynomial.natDegree_cubic_le Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} {a b c d : R} [inst : Semiring R], (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).natDegree ≤ 3
• Polynomial.degree_quadratic_lt_degree_C_mul_X_cb Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} {a b c d : R} [inst : Semiring R], a ≠ 0 → (Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree < (Polynomial.C a * Polynomial.X ^ 3).degree
• Polynomial.leadingCoeff_cubic Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} {a b c d : R} [inst : Semiring R], a ≠ 0 → (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).leadingCoeff = a
• Polynomial.natDegree_cubic Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} {a b c d : R} [inst : Semiring R], a ≠ 0 → (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).natDegree = 3
• Polynomial.degree_cubic_le Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} {a b c d : R} [inst : Semiring R], (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree ≤ 3
• Polynomial.degree_cubic_lt Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} {a b c d : R} [inst : Semiring R], (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree < 4
• Polynomial.degree_cubic Mathlib.Algebra.Polynomial.Degree.Definitions
  ∀ {R : Type u} {a b c d : R} [inst : Semiring R], a ≠ 0 → (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree = 3
• Polynomial.induction_on Mathlib.Algebra.Polynomial.Induction
  ∀ {R : Type u} [inst : Semiring R] {M : Polynomial R → Prop} (p : Polynomial R), (∀ (a : R), M (Polynomial.C a)) → (∀ (p q : Polynomial R), M p → M q → M (p + q)) → (∀ (n : ℕ) (a : R), M (Polynomial.C a * Polynomial.X ^ n) → M (Polynomial.C a * Polynomial.X ^ (n + 1))) → M p
• Polynomial.eval_eq_sum Mathlib.Algebra.Polynomial.Eval
  ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {x : R}, Polynomial.eval x p = p.sum fun e a => a * x ^ e
• Polynomial.eval_eq_sum_range' Mathlib.Algebra.Polynomial.Eval
  ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.natDegree < n → ∀ (x : R), Polynomial.eval x p = ∑ i ∈ Finset.range n, p.coeff i * x ^ i
• Polynomial.eval_eq_sum_range Mathlib.Algebra.Polynomial.Eval
  ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} (x : R), Polynomial.eval x p = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i * x ^ i
• Polynomial.coeff_comp_degree_mul_degree Mathlib.Algebra.Polynomial.Eval
  ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, q.natDegree ≠ 0 → (p.comp q).coeff (p.natDegree * q.natDegree) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
• Polynomial.eval₂_def Mathlib.Algebra.Polynomial.Eval
  ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S) (p : Polynomial R), Polynomial.eval₂ f x p = p.sum fun e a => f a * x ^ e
• Polynomial.eval₂_eq_sum Mathlib.Algebra.Polynomial.Eval
  ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] {f : R →+* S} {x : S}, Polynomial.eval₂ f x p = p.sum fun e a => f a * x ^ e
• Polynomial.eval_mul_X_pow Mathlib.Algebra.Polynomial.Eval
  ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {x : R} {k : ℕ}, Polynomial.eval x (p * Polynomial.X ^ k) = Polynomial.eval x p * x ^ k
• Polynomial.eval₂_eq_sum_range' Mathlib.Algebra.Polynomial.Eval
  ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) {p : Polynomial R} {n : ℕ}, p.natDegree < n → ∀ (x : S), Polynomial.eval₂ f x p = ∑ i ∈ Finset.range n, f (p.coeff i) * x ^ i
• Polynomial.eval₂_eq_sum_range Mathlib.Algebra.Polynomial.Eval
  ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (x : S), Polynomial.eval₂ f x p = ∑ i ∈ Finset.range (p.natDegree + 1), f (p.coeff i) * x ^ i
• Polynomial.mul_X_pow_comp Mathlib.Algebra.Polynomial.Eval
  ∀ {R : Type u} [inst : Semiring R] {p r : Polynomial R} {k : ℕ}, (p * Polynomial.X ^ k).comp r = p.comp r * r ^ k
• Polynomial.comp_eq_sum_left Mathlib.Algebra.Polynomial.Eval
  ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.comp q = p.sum fun e a => Polynomial.C a * q ^ e
• Polynomial.eval_monomial Mathlib.Algebra.Polynomial.Eval
  ∀ {R : Type u} [inst : Semiring R] {x : R} {n : ℕ} {a : R}, Polynomial.eval x ((Polynomial.monomial n) a) = a * x ^ n
• Polynomial.eval₂_monomial Mathlib.Algebra.Polynomial.Eval
  ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S) {n : ℕ} {r : R}, Polynomial.eval₂ f x ((Polynomial.monomial n) r) = f r * x ^ n
• Polynomial.monomial_comp Mathlib.Algebra.Polynomial.Eval
  ∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R} (n : ℕ), ((Polynomial.monomial n) a).comp p = Polynomial.C a * p ^ n
• Polynomial.eval_monomial_one_add_sub Mathlib.Algebra.Polynomial.Eval
  ∀ {S : Type v} [inst : CommRing S] (d : ℕ) (y : S), Polynomial.eval (1 + y) ((Polynomial.monomial d) (↑d + 1)) - Polynomial.eval y ((Polynomial.monomial d) (↑d + 1)) = ∑ x_1 ∈ Finset.range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
• Polynomial.dvd_term_of_isRoot_of_dvd_terms Mathlib.Algebra.Polynomial.AlgebraMap
  ∀ {S : Type v} [inst : CommRing S] {r p : S} {f : Polynomial S} (i : ℕ), f.IsRoot r → (∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * r ^ j) → p ∣ f.coeff i * r ^ i
• Polynomial.dvd_term_of_dvd_eval_of_dvd_terms Mathlib.Algebra.Polynomial.AlgebraMap
  ∀ {S : Type v} [inst : CommRing S] {z p : S} {f : Polynomial S} (i : ℕ), p ∣ Polynomial.eval z f → (∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j) → p ∣ f.coeff i * z ^ i
• Polynomial.aeval_monomial Mathlib.Algebra.Polynomial.AlgebraMap
  ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A) {n : ℕ} {r : R}, (Polynomial.aeval x) ((Polynomial.monomial n) r) = (algebraMap R A) r * x ^ n
• Polynomial.leadingCoeff_comp Mathlib.Algebra.Polynomial.Degree.Lemmas
  ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} [inst_1 : NoZeroDivisors R], q.natDegree ≠ 0 → (p.comp q).leadingCoeff = p.leadingCoeff * q.leadingCoeff ^ p.natDegree

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from witin the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
woould find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision f46663a serving mathlib revision c9428b0