Loogle!

Result

Found 2828 definitions mentioning HMul.hMul and HPow.hPow. Of these, 1319 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 : ℕ} (h : 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} [Monoid M] (a : M) (n : ℕ) : a ^ n * a = a * a ^ n
• pow_succ' 📋 Mathlib.Algebra.Group.Defs
  {M : Type u_2} [Monoid M] (a : M) (n : ℕ) : a ^ (n + 1) = a * a ^ n
• pow_add 📋 Mathlib.Algebra.Group.Defs
  {M : Type u_2} [Monoid M] (a : M) (m n : ℕ) : a ^ (m + n) = a ^ m * a ^ n
• pow_mul_comm 📋 Mathlib.Algebra.Group.Defs
  {M : Type u_2} [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} [Monoid M] {a b : M} (h : Commute a b) (n : ℕ) : (a * b) ^ n = a ^ n * b ^ n
• Commute.mul_zpow 📋 Mathlib.Algebra.Group.Commute.Defs
  {G : Type u_1} [DivisionMonoid G] {a b : G} (h : Commute a b) (n : ℤ) : (a * b) ^ n = a ^ n * b ^ n
• Nat.mul_lt_mul_pow_succ 📋 Mathlib.Data.Nat.Defs
  {a b n : ℕ} (ha : 0 < a) (hb : 1 < b) : n * b < a * b ^ (n + 1)
• mul_pow_sub_one 📋 Mathlib.Algebra.Group.Basic
  {M : Type u_4} [Monoid M] {n : ℕ} (hn : n ≠ 0) (a : M) : a * a ^ (n - 1) = a ^ n
• mul_self_zpow 📋 Mathlib.Algebra.Group.Basic
  {G : Type u_3} [Group G] (a : G) (n : ℤ) : a * a ^ n = a ^ (n + 1)
• zpow_one_add 📋 Mathlib.Algebra.Group.Basic
  {G : Type u_3} [Group G] (a : G) (n : ℤ) : a ^ (1 + n) = a * a ^ n
• pow_mul_pow_sub 📋 Mathlib.Algebra.Group.Basic
  {M : Type u_4} [Monoid M] {m n : ℕ} (a : M) (h : m ≤ n) : a ^ m * a ^ (n - m) = a ^ n
• pow_sub_mul_pow 📋 Mathlib.Algebra.Group.Basic
  {M : Type u_4} [Monoid M] {m n : ℕ} (a : M) (h : m ≤ n) : a ^ (n - m) * a ^ m = a ^ n
• zpow_add 📋 Mathlib.Algebra.Group.Basic
  {G : Type u_3} [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} [Monoid M] {a b : M} (n : ℕ) : a * b = 1 → a ^ n * b ^ n = 1
• mul_pow 📋 Mathlib.Algebra.Group.Basic
  {M : Type u_4} [CommMonoid M] (a b : M) (n : ℕ) : (a * b) ^ n = a ^ n * b ^ n
• mul_zpow 📋 Mathlib.Algebra.Group.Basic
  {α : Type u_1} [DivisionCommMonoid α] (a b : α) (n : ℤ) : (a * b) ^ n = a ^ n * b ^ n
• zpow_mul_comm 📋 Mathlib.Algebra.Group.Basic
  {G : Type u_3} [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} [DivisionMonoid α] (a b : α) : (a * b) ^ (-1) = b ^ (-1) * a ^ (-1)
• inv_pow_sub 📋 Mathlib.Algebra.Group.Basic
  {G : Type u_3} [Group G] (a : G) {m n : ℕ} (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
• mul_right_iterate 📋 Mathlib.Algebra.GroupPower.IterateHom
  {G : Type u_2} [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} [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) (i : ℤ) : a ^ (1 + i) = a * a ^ i
• zpow_add₀ 📋 Mathlib.Algebra.GroupWithZero.Basic
  {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n
• zpow_add' 📋 Mathlib.Algebra.GroupWithZero.Basic
  {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} {m n : ℤ} (h : 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} [GroupWithZero G₀] {a : G₀} (n : ℤ) (ha : a ≠ 0) : a ^ (-n) * a ^ n = 1
• inv_pow_sub_of_lt 📋 Mathlib.Algebra.GroupWithZero.Units.Basic
  {G₀ : Type u_3} [GroupWithZero G₀] {m n : ℕ} (a : G₀) (h : n < m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
• inv_pow_sub₀ 📋 Mathlib.Algebra.GroupWithZero.Units.Basic
  {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {m n : ℕ} (ha : a ≠ 0) (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
• Units.conj_pow 📋 Mathlib.Algebra.Group.Semiconj.Units
  {M : Type u_1} [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} [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} [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} [Ring R] {a : R} {n : ℕ} : a * (-1) ^ n = 0 ↔ a = 0
• neg_pow 📋 Mathlib.Algebra.Ring.Commute
  {R : Type u} [Monoid R] [HasDistribNeg R] (a : R) (n : ℕ) : (-a) ^ n = (-1) ^ n * a ^ n
• neg_pow' 📋 Mathlib.Algebra.Ring.Commute
  {R : Type u} [Monoid R] [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} [Semiring α] [LinearOrder α] {a b : α} [PosMulStrictMono α] (h : ∀ (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} [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} [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} [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} [OrderedSemiring R] {a b : R} {n : ℕ} (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ n + b ^ n ≤ 2 * (a + b) ^ n
• CancelDenoms.pow_subst 📋 Mathlib.Tactic.CancelDenoms.Core
  {α : Type u_1} [CommRing α] {n e1 t1 k l : α} {e2 : ℕ} (h1 : n * e1 = t1) (h2 : l * n ^ e2 = k) : k * e1 ^ e2 = l * t1 ^ e2
• 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} [Group G] (a : G) (m n : ℕ) : a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m
• Nat.factorial_mul_pow_sub_le_factorial 📋 Mathlib.Data.Nat.Factorial.Basic
  {n m : ℕ} (hnm : 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} [LinearOrderedCommGroup α] [MulArchimedean α] {a : α} (ha : 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} [LinearOrderedCommGroup α] [MulArchimedean α] {a : α} (ha : 1 < a) (b c : α) : ∃! m, b * a ^ m ∈ Set.Ico c (c * a)
• List.alternatingProd_append 📋 Mathlib.Algebra.BigOperators.Group.List
  {α : Type u_2} [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 : α → β} [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} [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} [Group α] {i : ℤ} {a b : α} : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
• conj_pow 📋 Mathlib.Algebra.Group.Conj
  {α : Type u} [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} [CommGroup C] {x y z : C} : z ∈ Subgroup.closure {x, y} ↔ ∃ m n, x ^ m * y ^ n = z
• Algebra.mul_sub_algebraMap_pow_commutes 📋 Mathlib.Algebra.Algebra.Basic
  {R : Type u} {A : Type w} [CommSemiring R] [Ring A] [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} [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} [CommSemiring α] (ι : Type u_7) [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 : ℕ} [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} [CommSemiring R] (a b : R) : ∑ s : Finset (Fin n), a ^ s.card * b ^ (n - s.card) = (a + b) ^ n
• Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd 📋 Mathlib.Algebra.Prime.Lemmas
  {M : Type u_1} [CancelCommMonoidWithZero M] {p a b : M} {n : ℕ} (hp : Prime p) (hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n) (hb : ¬p ^ 2 ∣ b) : p ∣ a
• Submodule.pow_induction_on_left' 📋 Mathlib.Algebra.Algebra.Operations
  {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) {C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop} (algebraMap : ∀ (r : R), C 0 ((algebraMap R A) r) ⋯) (add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯) (mem_mul : ∀ (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
• Commute.add_pow' 📋 Mathlib.Data.Nat.Choose.Sum
  {R : Type u_1} [Semiring R] {x y : R} (h : 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} [Semiring R] {x y : R} (h : 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} [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} [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)
• 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}} (a0 : 0 < a) (h : 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}} (a0 : 0 < a) (h : 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} [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} [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} [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} [Group α] (H : Subgroup α) (a : α) (q : α ⧸ H) : (Quotient.out q)⁻¹ * a ^ Function.minimalPeriod (fun x => a • x) q * Quotient.out q ∈ H
• QuotientGroup.out_conj_pow_minimalPeriod_mem 📋 Mathlib.GroupTheory.GroupAction.Quotient
  {α : Type u} [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} [MulOneClass M] [Pow M ℕ] [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✝¹ : 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} [MulOneClass M] [Pow M ℕ] [NatPowAssoc M] (m n : ℕ) (x : M) : x ^ m * x ^ n = x ^ n * x ^ m
• NatPowAssoc.mk 📋 Mathlib.Algebra.Group.NatPowAssoc
  {M : Type u_2} [MulOneClass M] [Pow M ℕ] (npow_add : ∀ (k n : ℕ) (x : M), x ^ (k + n) = x ^ k * x ^ n) (npow_zero : ∀ (x : M), x ^ 0 = 1) (npow_one : ∀ (x : M), x ^ 1 = x) : NatPowAssoc M
• npow_mul_assoc 📋 Mathlib.Algebra.Group.NatPowAssoc
  {M : Type u_1} [MulOneClass M] [Pow M ℕ] [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} [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} [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} [Ring α] {x y : α} (h : 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} [Ring α] {x y : α} (h : 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} [Ring α] {x y : α} (h : 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} [Semiring α] {x y : α} (n : ℕ) (h : 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} [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} [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} [DivisionRing α] {x y : α} (h' : Commute x y) (h : 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} [Semiring α] {x y : α} (h : 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} [Field α] {x y : α} (h : 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} [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} [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} [Ring α] {x y : α} (h : Commute x y) {m n : ℕ} (hmn : 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} [Ring α] {x y : α} (h : Commute x y) {m n : ℕ} (hmn : 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} [CommRing α] (x y : α) {m n : ℕ} (hmn : 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} [Ring α] {x y : α} (h : 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)
• geom₂_sum_of_gt 📋 Mathlib.Algebra.GeomSum
  {α : Type u_1} [CanonicallyLinearOrderedSemifield α] [Sub α] [OrderedSub α] {x y : α} (h : y < x) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
• geom₂_sum_of_lt 📋 Mathlib.Algebra.GeomSum
  {α : Type u_1} [CanonicallyLinearOrderedSemifield α] [Sub α] [OrderedSub α] {x y : α} (h : x < y) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (y ^ n - x ^ n) / (y - x)
• RingHom.map_geom_sum₂ 📋 Mathlib.Algebra.GeomSum
  {α : Type u} {β : Type u_1} [Semiring α] [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₂_mul_of_ge 📋 Mathlib.Algebra.GeomSum
  {α : Type u} [CommSemiring α] [PartialOrder α] [AddLeftReflectLE α] [AddLeftMono α] [ExistsAddOfLE α] [Sub α] [OrderedSub α] {x y : α} (hxy : y ≤ x) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
• geom_sum₂_mul_of_le 📋 Mathlib.Algebra.GeomSum
  {α : Type u} [CommSemiring α] [PartialOrder α] [AddLeftReflectLE α] [AddLeftMono α] [ExistsAddOfLE α] [Sub α] [OrderedSub α] {x y : α} (hxy : x ≤ y) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (y - x) = y ^ n - x ^ n
• geom_sum₂_succ_eq 📋 Mathlib.Algebra.GeomSum
  {α : Type u} [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} [DivisionRing α] {x y : α} (h : Commute x y) (hxy : x ≠ y) {m n : ℕ} (hmn : 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} [Field α] {x y : α} (hxy : x ≠ y) {m n : ℕ} (hmn : 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_mul_pow_sub_pow_div_expChar_of_commute 📋 Mathlib.Algebra.CharP.Lemmas
  {R : Type u_1} [Ring R] {x y : R} (p n : ℕ) [hR : ExpChar R p] (h : Commute x y) : (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
• sub_pow_eq_mul_pow_sub_pow_div_char_of_commute 📋 Mathlib.Algebra.CharP.Lemmas
  (R : Type u_1) [Ring R] {x y : R} (p n : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] (h : Commute x y) : (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
• sub_pow_eq_mul_pow_sub_pow_div_expChar 📋 Mathlib.Algebra.CharP.Lemmas
  {R : Type u_1} [CommRing R] (x y : R) (n : ℕ) {p : ℕ} [hR : ExpChar R p] : (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
• add_pow_eq_mul_pow_add_pow_div_expChar_of_commute 📋 Mathlib.Algebra.CharP.Lemmas
  {R : Type u_1} [Semiring R] {x y : R} (p n : ℕ) [hR : ExpChar R p] (h : Commute x y) : (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
• sub_pow_eq_mul_pow_sub_pow_div_char 📋 Mathlib.Algebra.CharP.Lemmas
  {R : Type u_1} [CommRing R] (x y : R) (n : ℕ) {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] : (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
• add_pow_eq_mul_pow_add_pow_div_char_of_commute 📋 Mathlib.Algebra.CharP.Lemmas
  {R : Type u_1} [Semiring R] {x y : R} (p n : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] (h : Commute x y) : (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
• add_pow_eq_mul_pow_add_pow_div_expChar 📋 Mathlib.Algebra.CharP.Lemmas
  {R : Type u_1} [CommSemiring R] (x y : R) (p n : ℕ) [hR : ExpChar 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.Lemmas
  {R : Type u_1} [CommSemiring R] (x y : R) (p n : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] : (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
• add_pow_eq_mul_pow_add_pow_div_char 📋 Mathlib.Algebra.CharP.Lemmas
  {R : Type u_1} [CommSemiring R] (x y : R) (p n : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] : (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
• Commute.add_pow_prime_eq 📋 Mathlib.Algebra.CharP.Lemmas
  {R : Type u_1} [Semiring R] {p : ℕ} (hp : Nat.Prime p) {x y : R} (h : 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.Lemmas
  {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : 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.Lemmas
  {R : Type u_1} [Semiring R] {p : ℕ} (hp : Nat.Prime p) {x y : R} (h : 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.Lemmas
  {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : 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.ordProj_mul 📋 Mathlib.Data.Nat.Factorization.Basic
  {a b : ℕ} (p : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) : p ^ (a * b).factorization p = p ^ a.factorization p * p ^ b.factorization p
• Nat.ord_proj_mul 📋 Mathlib.Data.Nat.Factorization.Basic
  {a b : ℕ} (p : ℕ) (ha : a ≠ 0) (hb : 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} [CommSemiring R] [Module R (Additive ℤˣ)] (s : ℤˣ) (x y : R) : s ^ (x + y) = s ^ x * s ^ y
• mul_uzpow 📋 Mathlib.Data.ZMod.IntUnitsPower
  {R : Type u_1} [CommSemiring R] [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 : ℕ} (hp : Nat.Prime p) (h : ↑p ∣ 2 * m ^ 2) : p = 2 ∨ p ∣ m.natAbs
• Commute.orderOf_mul_pow_eq_lcm 📋 Mathlib.GroupTheory.Exponent
  {G : Type u} [Monoid G] {x y : G} (h : Commute x y) (hx : orderOf x ≠ 0) (hy : 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} [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 : σ →₀ ℕ} [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} [Semiring R] (n : ℕ) (c : R) : (Polynomial.C c * Polynomial.X ^ n).support ⊆ {n}
• Polynomial.X_pow_mul 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [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} [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} [Semiring R] (n : ℕ) {c : R} (h : c ≠ 0) : (Polynomial.C c * Polynomial.X ^ n).support = {n}
• Polynomial.sum_C_mul_X_pow_eq 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [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} [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} [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} [Semiring R] {n : ℕ} : Polynomial.C a * Polynomial.X ^ n = (Polynomial.monomial n) a
• Polynomial.support_binomial' 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [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} [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} [Semiring R] (n : ℕ) (r : R) (k : ℕ) : (Polynomial.monomial n) r * Polynomial.X ^ k = (Polynomial.monomial (n + k)) r
• Polynomial.induction_on 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [Semiring R] {M : Polynomial R → Prop} (p : Polynomial R) (h_C : ∀ (a : R), M (Polynomial.C a)) (h_add : ∀ (p q : Polynomial R), M p → M q → M (p + q)) (h_monomial : ∀ (n : ℕ) (a : R), M (Polynomial.C a * Polynomial.X ^ n) → M (Polynomial.C a * Polynomial.X ^ (n + 1))) : M p
• Polynomial.support_trinomial' 📋 Mathlib.Algebra.Polynomial.Basic
  {R : Type u} [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} [Semiring R] {k l m n : ℕ} {u v : R} (hu : u ≠ 0) (hv : 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.eval_eq_sum 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {x : R} : Polynomial.eval x p = p.sum fun e a => a * x ^ e
• Polynomial.eval₂_def 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u_1} {S : Type u_2} [Semiring R] [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.Defs
  {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [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.Defs
  {R : Type u} [Semiring R] {p : Polynomial R} {x : R} {k : ℕ} : Polynomial.eval x (p * Polynomial.X ^ k) = Polynomial.eval x p * x ^ k
• Polynomial.mul_X_pow_comp 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} [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.Defs
  {R : Type u} [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.Defs
  {R : Type u} [Semiring R] {x : R} {n : ℕ} {a : R} : Polynomial.eval x ((Polynomial.monomial n) a) = a * x ^ n
• Polynomial.eval₂_monomial 📋 Mathlib.Algebra.Polynomial.Eval.Defs
  {R : Type u} {S : Type v} [Semiring R] [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.Defs
  {R : Type u} {a : R} [Semiring R] {p : Polynomial R} (n : ℕ) : ((Polynomial.monomial n) a).comp p = Polynomial.C a * p ^ n
• Polynomial.coeff_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [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} [Semiring R] {p : Polynomial R} {n : ℕ} (H : p * Polynomial.X ^ n = 0) : p = 0
• Polynomial.coeff_mul_X_pow' 📋 Mathlib.Algebra.Polynomial.Coeff
  {R : Type u} [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} [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} [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} [Semiring R] {k m : ℕ} (h : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : 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} [Semiring R] {k m : ℕ} (hkm : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : 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} [Semiring R] {k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x ≠ 0) (hy : y ≠ 0) (hz : 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} [Semiring R] {k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x ≠ 0) (hy : y ≠ 0) (hz : 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_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Definitions
  {R : Type u} [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} [Semiring R] (a : R) (n : ℕ) : (Polynomial.C a * Polynomial.X ^ n).natDegree ≤ n
• Polynomial.natDegree_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Definitions
  {R : Type u} [Semiring R] (n : ℕ) (a : R) (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ n).natDegree = n
• Polynomial.degree_C_mul_X_pow_le 📋 Mathlib.Algebra.Polynomial.Degree.Definitions
  {R : Type u} [Semiring R] (n : ℕ) (a : R) : (Polynomial.C a * Polynomial.X ^ n).degree ≤ ↑n
• Polynomial.degree_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Definitions
  {R : Type u} {a : R} [Semiring R] (n : ℕ) (ha : a ≠ 0) : (Polynomial.C a * Polynomial.X ^ n).degree = ↑n
• Polynomial.leadingCoeff_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : (p * Polynomial.X ^ n).leadingCoeff = p.leadingCoeff
• Polynomial.natDegree_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (n : ℕ) (hp : p ≠ 0) : (p * Polynomial.X ^ n).natDegree = p.natDegree + n
• Polynomial.degree_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] [Nontrivial R] {p : Polynomial R} (n : ℕ) : (p * Polynomial.X ^ n).degree = p.degree + ↑n
• Polynomial.degree_sum_fin_lt 📋 Mathlib.Algebra.Polynomial.Degree.Operations
  {R : Type u} [Semiring R] {n : ℕ} (f : Fin n → R) : (∑ i : Fin n, Polynomial.C (f i) * Polynomial.X ^ ↑i).degree < ↑n
• Polynomial.card_support_C_mul_X_pow_le_one 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [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.Support
  {R : Type u} [Semiring R] {n a : ℕ} {c : R} (h : a ∈ (Polynomial.C c * Polynomial.X ^ n).support) : a = n
• Polynomial.as_sum_support_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] (p : Polynomial R) : p = ∑ i ∈ p.support, Polynomial.C (p.coeff i) * Polynomial.X ^ i
• Polynomial.as_sum_range_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Support
  {R : Type u} [Semiring R] (p : Polynomial R) : p = ∑ i ∈ Finset.range (p.natDegree + 1), Polynomial.C (p.coeff i) * Polynomial.X ^ i
• Polynomial.natDegree_quadratic_le 📋 Mathlib.Algebra.Polynomial.Degree.SmallDegree
  {R : Type u} {a b c : R} [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.SmallDegree
  {R : Type u} {a b c : R} [Semiring R] (ha : 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.SmallDegree
  {R : Type u} {a b c : R} [Semiring R] (ha : 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.SmallDegree
  {R : Type u} {a b c : R} [Semiring R] (ha : 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.SmallDegree
  {R : Type u} {a b c : R} [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.SmallDegree
  {R : Type u} {a b c : R} [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.SmallDegree
  {R : Type u} {a b c : R} [Semiring R] (ha : 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.SmallDegree
  {R : Type u} {a b c d : R} [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.SmallDegree
  {R : Type u} {a b c d : R} [Semiring R] (ha : 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.SmallDegree
  {R : Type u} {a b c d : R} [Semiring R] (ha : 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.SmallDegree
  {R : Type u} {a b c d : R} [Semiring R] (ha : 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.SmallDegree
  {R : Type u} {a b c d : R} [Semiring R] : (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree ≤ 3

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, 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 4e1aab0 serving mathlib revision 79ca167