Loogle!

Result

Found 146 declarations mentioning Nat.factorization.

• Nat.factorization 📋 Mathlib.Data.Nat.Factorization.Defs
  (n : ℕ) : ℕ →₀ ℕ
• Nat.support_factorization 📋 Mathlib.Data.Nat.Factorization.Defs
  (n : ℕ) : n.factorization.support = n.primeFactors
• Nat.factorization_inj 📋 Mathlib.Data.Nat.Factorization.Defs
  : Set.InjOn Nat.factorization {x | x ≠ 0}
• Nat.Prime.factorization 📋 Mathlib.Data.Nat.Factorization.Defs
  {p : ℕ} (hp : Nat.Prime p) : p.factorization = fun₀ | p => 1
• Nat.factorization_def 📋 Mathlib.Data.Nat.Factorization.Defs
  (n : ℕ) {p : ℕ} (pp : Nat.Prime p) : n.factorization p = padicValNat p n
• Nat.factorization_eq_zero_of_non_prime 📋 Mathlib.Data.Nat.Factorization.Defs
  (n : ℕ) {p : ℕ} (hp : ¬Nat.Prime p) : n.factorization p = 0
• Nat.factorization_zero_right 📋 Mathlib.Data.Nat.Factorization.Defs
  (n : ℕ) : n.factorization 0 = 0
• Nat.primeFactorsList_count_eq 📋 Mathlib.Data.Nat.Factorization.Defs
  {n p : ℕ} : List.count p n.primeFactorsList = n.factorization p
• Nat.Prime.factorization_pow 📋 Mathlib.Data.Nat.Factorization.Defs
  {p k : ℕ} (hp : Nat.Prime p) : (p ^ k).factorization = fun₀ | p => k
• Nat.factorization_eq_zero_of_not_dvd 📋 Mathlib.Data.Nat.Factorization.Defs
  {n p : ℕ} (h : ¬p ∣ n) : n.factorization p = 0
• Nat.factorization_one 📋 Mathlib.Data.Nat.Factorization.Defs
  : Nat.factorization 1 = 0
• Nat.factorization_zero 📋 Mathlib.Data.Nat.Factorization.Defs
  : Nat.factorization 0 = 0
• Nat.factorization.eq_1 📋 Mathlib.Data.Nat.Factorization.Defs
  (n : ℕ) : n.factorization = { support := n.primeFactors, toFun := fun p => if Nat.Prime p then padicValNat p n else 0, mem_support_toFun := ⋯ }
• Nat.factorization_prod_pow_eq_self 📋 Mathlib.Data.Nat.Factorization.Defs
  {n : ℕ} (hn : n ≠ 0) : (n.factorization.prod fun x1 x2 => x1 ^ x2) = n
• Nat.ordProj_dvd 📋 Mathlib.Data.Nat.Factorization.Defs
  (n p : ℕ) : p ^ n.factorization p ∣ n
• Nat.ord_proj_dvd 📋 Mathlib.Data.Nat.Factorization.Defs
  (n p : ℕ) : p ^ n.factorization p ∣ n
• Nat.multiplicity_eq_factorization 📋 Mathlib.Data.Nat.Factorization.Defs
  {n p : ℕ} (pp : Nat.Prime p) (hn : n ≠ 0) : multiplicity p n = n.factorization p
• Nat.factorization_le_iff_dvd 📋 Mathlib.Data.Nat.Factorization.Defs
  {d n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) : d.factorization ≤ n.factorization ↔ d ∣ n
• Nat.Prime.factorization_pos_of_dvd 📋 Mathlib.Data.Nat.Factorization.Defs
  {n p : ℕ} (hp : Nat.Prime p) (hn : n ≠ 0) (h : p ∣ n) : 0 < n.factorization p
• Nat.factorization_eq_zero_iff 📋 Mathlib.Data.Nat.Factorization.Defs
  (n p : ℕ) : n.factorization p = 0 ↔ ¬Nat.Prime p ∨ ¬p ∣ n ∨ n = 0
• Nat.factorization_eq_zero_of_remainder 📋 Mathlib.Data.Nat.Factorization.Defs
  {p r : ℕ} (i : ℕ) (hr : ¬p ∣ r) : (p * i + r).factorization p = 0
• Nat.factorization_pow 📋 Mathlib.Data.Nat.Factorization.Defs
  (n k : ℕ) : (n ^ k).factorization = k • n.factorization
• Nat.factorization_prod 📋 Mathlib.Data.Nat.Factorization.Defs
  {α : Type u_1} {S : Finset α} {g : α → ℕ} (hS : ∀ x ∈ S, g x ≠ 0) : (S.prod g).factorization = ∑ x ∈ S, (g x).factorization
• Nat.prod_pow_factorization_eq_self 📋 Mathlib.Data.Nat.Factorization.Defs
  {f : ℕ →₀ ℕ} (hf : ∀ p ∈ f.support, Nat.Prime p) : (f.prod fun x1 x2 => x1 ^ x2).factorization = f
• Nat.factorization_mul_of_coprime 📋 Mathlib.Data.Nat.Factorization.Defs
  {a b : ℕ} (hab : a.Coprime b) : (a * b).factorization = a.factorization + b.factorization
• Nat.pow_succ_factorization_not_dvd 📋 Mathlib.Data.Nat.Factorization.Defs
  {n p : ℕ} (hn : n ≠ 0) (hp : Nat.Prime p) : ¬p ^ (n.factorization p + 1) ∣ n
• Nat.eq_of_factorization_eq 📋 Mathlib.Data.Nat.Factorization.Defs
  {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (h : ∀ (p : ℕ), a.factorization p = b.factorization p) : a = b
• Nat.factorization_mul 📋 Mathlib.Data.Nat.Factorization.Defs
  {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : (a * b).factorization = a.factorization + b.factorization
• Nat.factorization_mul_apply_of_coprime 📋 Mathlib.Data.Nat.Factorization.Defs
  {p a b : ℕ} (hab : a.Coprime b) : (a * b).factorization p = a.factorization p + b.factorization p
• Nat.factorization_eq_primeFactorsList_multiset 📋 Mathlib.Data.Nat.Factorization.Defs
  (n : ℕ) : n.factorization = Multiset.toFinsupp ↑n.primeFactorsList
• Nat.Prime.factorization_self 📋 Mathlib.Data.Nat.Factorization.Basic
  {p : ℕ} (hp : Nat.Prime p) : p.factorization p = 1
• Nat.factorization_one_right 📋 Mathlib.Data.Nat.Factorization.Basic
  (n : ℕ) : n.factorization 1 = 0
• Nat.prod_primeFactors_prod_factorization 📋 Mathlib.Data.Nat.Factorization.Basic
  {n : ℕ} {β : Type u_1} [CommMonoid β] (f : ℕ → β) : ∏ p ∈ n.primeFactors, f p = n.factorization.prod fun p x => f p
• Nat.dvd_of_factorization_pos 📋 Mathlib.Data.Nat.Factorization.Basic
  {n p : ℕ} (hn : n.factorization p ≠ 0) : p ∣ n
• Nat.factorization_eq_zero_of_lt 📋 Mathlib.Data.Nat.Factorization.Basic
  {n p : ℕ} (h : n < p) : n.factorization p = 0
• Nat.factorization_lt 📋 Mathlib.Data.Nat.Factorization.Basic
  {n : ℕ} (p : ℕ) (hn : n ≠ 0) : n.factorization p < n
• Nat.Prime.eq_of_factorization_pos 📋 Mathlib.Data.Nat.Factorization.Basic
  {p q : ℕ} (hp : Nat.Prime p) (h : p.factorization q ≠ 0) : p = q
• Nat.factorization_le_factorization_mul_left 📋 Mathlib.Data.Nat.Factorization.Basic
  {a b : ℕ} (hb : b ≠ 0) : a.factorization ≤ (a * b).factorization
• Nat.factorization_le_factorization_mul_right 📋 Mathlib.Data.Nat.Factorization.Basic
  {a b : ℕ} (ha : a ≠ 0) : b.factorization ≤ (a * b).factorization
• Nat.ordProj_pos 📋 Mathlib.Data.Nat.Factorization.Basic
  (n p : ℕ) : 0 < p ^ n.factorization p
• Nat.ord_proj_pos 📋 Mathlib.Data.Nat.Factorization.Basic
  (n p : ℕ) : 0 < p ^ n.factorization p
• Nat.factorization_le_of_le_pow 📋 Mathlib.Data.Nat.Factorization.Basic
  {n p b : ℕ} (hb : n ≤ p ^ b) : n.factorization p ≤ b
• Nat.ordProj_of_not_prime 📋 Mathlib.Data.Nat.Factorization.Basic
  (n p : ℕ) (hp : ¬Nat.Prime p) : p ^ n.factorization p = 1
• Nat.ord_proj_of_not_prime 📋 Mathlib.Data.Nat.Factorization.Basic
  (n p : ℕ) (hp : ¬Nat.Prime p) : p ^ n.factorization p = 1
• Nat.eq_pow_of_factorization_eq_single 📋 Mathlib.Data.Nat.Factorization.Basic
  {n p k : ℕ} (hn : n ≠ 0) (h : n.factorization = fun₀ | p => k) : n = p ^ k
• Nat.ordCompl_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  (n p : ℕ) : n / p ^ n.factorization p ∣ n
• Nat.ordCompl_le 📋 Mathlib.Data.Nat.Factorization.Basic
  (n p : ℕ) : n / p ^ n.factorization p ≤ n
• Nat.ordProj_le 📋 Mathlib.Data.Nat.Factorization.Basic
  {n : ℕ} (p : ℕ) (hn : n ≠ 0) : p ^ n.factorization p ≤ n
• Nat.ord_compl_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  (n p : ℕ) : n / p ^ n.factorization p ∣ n
• Nat.ord_compl_le 📋 Mathlib.Data.Nat.Factorization.Basic
  (n p : ℕ) : n / p ^ n.factorization p ≤ n
• Nat.ord_proj_le 📋 Mathlib.Data.Nat.Factorization.Basic
  {n : ℕ} (p : ℕ) (hn : n ≠ 0) : p ^ n.factorization p ≤ n
• Nat.Prime.dvd_iff_one_le_factorization 📋 Mathlib.Data.Nat.Factorization.Basic
  {p n : ℕ} (pp : Nat.Prime p) (hn : n ≠ 0) : p ∣ n ↔ 1 ≤ n.factorization p
• Nat.ordCompl_of_not_prime 📋 Mathlib.Data.Nat.Factorization.Basic
  (n p : ℕ) (hp : ¬Nat.Prime p) : n / p ^ n.factorization p = n
• Nat.ord_compl_of_not_prime 📋 Mathlib.Data.Nat.Factorization.Basic
  (n p : ℕ) (hp : ¬Nat.Prime p) : n / p ^ n.factorization p = n
• Nat.prod_factorization_eq_prod_primeFactors 📋 Mathlib.Data.Nat.Factorization.Basic
  {n : ℕ} {β : Type u_1} [CommMonoid β] (f : ℕ → ℕ → β) : n.factorization.prod f = ∏ p ∈ n.primeFactors, f p (n.factorization p)
• Nat.factorization_eq_zero_iff' 📋 Mathlib.Data.Nat.Factorization.Basic
  (n : ℕ) : n.factorization = 0 ↔ n = 0 ∨ n = 1
• Nat.dvd_ordProj_of_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  {n p : ℕ} (hn : n ≠ 0) (pp : Nat.Prime p) (h : p ∣ n) : p ∣ p ^ n.factorization p
• Nat.dvd_ord_proj_of_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  {n p : ℕ} (hn : n ≠ 0) (pp : Nat.Prime p) (h : p ∣ n) : p ∣ p ^ n.factorization p
• Nat.coprime_ordCompl 📋 Mathlib.Data.Nat.Factorization.Basic
  {n p : ℕ} (hp : Nat.Prime p) (hn : n ≠ 0) : p.Coprime (n / p ^ n.factorization p)
• Nat.coprime_ord_compl 📋 Mathlib.Data.Nat.Factorization.Basic
  {n p : ℕ} (hp : Nat.Prime p) (hn : n ≠ 0) : p.Coprime (n / p ^ n.factorization p)
• Nat.Prime.pow_dvd_iff_le_factorization 📋 Mathlib.Data.Nat.Factorization.Basic
  {p k n : ℕ} (pp : Nat.Prime p) (hn : n ≠ 0) : p ^ k ∣ n ↔ k ≤ n.factorization p
• Nat.not_dvd_ordCompl 📋 Mathlib.Data.Nat.Factorization.Basic
  {n p : ℕ} (hp : Nat.Prime p) (hn : n ≠ 0) : ¬p ∣ n / p ^ n.factorization p
• Nat.not_dvd_ord_compl 📋 Mathlib.Data.Nat.Factorization.Basic
  {n p : ℕ} (hp : Nat.Prime p) (hn : n ≠ 0) : ¬p ∣ n / p ^ n.factorization p
• Nat.dvd_ordCompl_of_dvd_not_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  {p d n : ℕ} (hdn : d ∣ n) (hpd : ¬p ∣ d) : d ∣ n / p ^ n.factorization p
• Nat.dvd_ord_compl_of_dvd_not_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  {p d n : ℕ} (hdn : d ∣ n) (hpd : ¬p ∣ d) : d ∣ n / p ^ n.factorization p
• Nat.ordCompl_pos 📋 Mathlib.Data.Nat.Factorization.Basic
  {n : ℕ} (p : ℕ) (hn : n ≠ 0) : 0 < n / p ^ n.factorization p
• Nat.ord_compl_pos 📋 Mathlib.Data.Nat.Factorization.Basic
  {n : ℕ} (p : ℕ) (hn : n ≠ 0) : 0 < n / p ^ n.factorization p
• Nat.factorization_ordCompl 📋 Mathlib.Data.Nat.Factorization.Basic
  (n p : ℕ) : (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization
• Nat.factorization_ord_compl 📋 Mathlib.Data.Nat.Factorization.Basic
  (n p : ℕ) : (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization
• Nat.factorization_gcd 📋 Mathlib.Data.Nat.Factorization.Basic
  {a b : ℕ} (ha_pos : a ≠ 0) (hb_pos : b ≠ 0) : (a.gcd b).factorization = a.factorization ⊓ b.factorization
• Nat.factorization_lcm 📋 Mathlib.Data.Nat.Factorization.Basic
  {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : (a.lcm b).factorization = a.factorization ⊔ b.factorization
• Nat.exists_factorization_lt_of_lt 📋 Mathlib.Data.Nat.Factorization.Basic
  {a b : ℕ} (ha : a ≠ 0) (hab : a < b) : ∃ p, a.factorization p < b.factorization p
• Nat.factorization_div 📋 Mathlib.Data.Nat.Factorization.Basic
  {d n : ℕ} (h : d ∣ n) : (n / d).factorization = n.factorization - d.factorization
• Nat.factorization_eq_zero_iff_remainder 📋 Mathlib.Data.Nat.Factorization.Basic
  {p r : ℕ} (i : ℕ) (pp : Nat.Prime p) (hr0 : r ≠ 0) : ¬p ∣ r ↔ (p * i + r).factorization p = 0
• Nat.factorization_eq_of_coprime_left 📋 Mathlib.Data.Nat.Factorization.Basic
  {p a b : ℕ} (hab : a.Coprime b) (hpa : p ∈ a.primeFactorsList) : (a * b).factorization p = a.factorization p
• Nat.factorization_eq_of_coprime_right 📋 Mathlib.Data.Nat.Factorization.Basic
  {p a b : ℕ} (hab : a.Coprime b) (hpb : p ∈ b.primeFactorsList) : (a * b).factorization p = b.factorization p
• Nat.factorization_prime_le_iff_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  {d n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) : (∀ (p : ℕ), Nat.Prime p → d.factorization p ≤ n.factorization p) ↔ d ∣ n
• Nat.eq_factorization_iff 📋 Mathlib.Data.Nat.Factorization.Basic
  {n : ℕ} {f : ℕ →₀ ℕ} (hn : n ≠ 0) (hf : ∀ p ∈ f.support, Nat.Prime p) : f = n.factorization ↔ (f.prod fun x1 x2 => x1 ^ x2) = n
• Nat.setOf_pow_dvd_eq_Icc_factorization 📋 Mathlib.Data.Nat.Factorization.Basic
  {n p : ℕ} (pp : Nat.Prime p) (hn : n ≠ 0) : {i | i ≠ 0 ∧ p ^ i ∣ n} = Set.Icc 1 (n.factorization p)
• Nat.factorization_eq_card_pow_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  (n : ℕ) {p : ℕ} (pp : Nat.Prime p) : n.factorization p = {i ∈ Finset.Ico 1 n | p ^ i ∣ n}.card
• Nat.Prime.pow_dvd_iff_dvd_ordProj 📋 Mathlib.Data.Nat.Factorization.Basic
  {p k n : ℕ} (pp : Nat.Prime p) (hn : n ≠ 0) : p ^ k ∣ n ↔ p ^ k ∣ p ^ n.factorization p
• Nat.Prime.pow_dvd_iff_dvd_ord_proj 📋 Mathlib.Data.Nat.Factorization.Basic
  {p k n : ℕ} (pp : Nat.Prime p) (hn : n ≠ 0) : p ^ k ∣ n ↔ p ^ k ∣ p ^ n.factorization p
• Nat.dvd_iff_div_factorization_eq_tsub 📋 Mathlib.Data.Nat.Factorization.Basic
  {d n : ℕ} (hd : d ≠ 0) (hdn : d ≤ n) : d ∣ n ↔ (n / d).factorization = n.factorization - d.factorization
• Nat.Icc_factorization_eq_pow_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  (n : ℕ) {p : ℕ} (pp : Nat.Prime p) : Finset.Icc 1 (n.factorization p) = {i ∈ Finset.Ico 1 n | p ^ i ∣ n}
• Nat.ordProj_dvd_ordProj_of_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  {a b : ℕ} (hb0 : b ≠ 0) (hab : a ∣ b) (p : ℕ) : p ^ a.factorization p ∣ p ^ b.factorization p
• Nat.ord_proj_dvd_ord_proj_of_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  {a b : ℕ} (hb0 : b ≠ 0) (hab : a ∣ b) (p : ℕ) : p ^ a.factorization p ∣ p ^ b.factorization p
• Nat.ordProj_mul_ordCompl_eq_self 📋 Mathlib.Data.Nat.Factorization.Basic
  (n p : ℕ) : p ^ n.factorization p * (n / p ^ n.factorization p) = n
• Nat.ord_proj_mul_ord_compl_eq_self 📋 Mathlib.Data.Nat.Factorization.Basic
  (n p : ℕ) : p ^ n.factorization p * (n / p ^ n.factorization p) = n
• Nat.ordCompl_dvd_ordCompl_of_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  {a b : ℕ} (hab : a ∣ b) (p : ℕ) : a / p ^ a.factorization p ∣ b / p ^ b.factorization p
• Nat.ord_compl_dvd_ord_compl_of_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  {a b : ℕ} (hab : a ∣ b) (p : ℕ) : a / p ^ a.factorization p ∣ b / p ^ b.factorization p
• Nat.ordCompl_dvd_ordCompl_iff_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  (a b : ℕ) : (∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p) ↔ a ∣ b
• Nat.ordProj_dvd_ordProj_iff_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  {a b : ℕ} (ha0 : a ≠ 0) (hb0 : b ≠ 0) : (∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p) ↔ a ∣ b
• Nat.ord_compl_dvd_ord_compl_iff_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  (a b : ℕ) : (∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p) ↔ a ∣ b
• Nat.ord_proj_dvd_ord_proj_iff_dvd 📋 Mathlib.Data.Nat.Factorization.Basic
  {a b : ℕ} (ha0 : a ≠ 0) (hb0 : b ≠ 0) : (∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p) ↔ a ∣ b
• Nat.factorizationLCMLeft.eq_1 📋 Mathlib.Data.Nat.Factorization.Basic
  (a b : ℕ) : a.factorizationLCMLeft b = (a.lcm b).factorization.prod fun p n => if b.factorization p ≤ a.factorization p then p ^ n else 1
• Nat.factorizationLCMRight.eq_1 📋 Mathlib.Data.Nat.Factorization.Basic
  (a b : ℕ) : a.factorizationLCMRight b = (a.lcm b).factorization.prod fun p n => if b.factorization p ≤ a.factorization p then 1 else p ^ n
• 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
• Nat.ordCompl_mul 📋 Mathlib.Data.Nat.Factorization.Basic
  (a b p : ℕ) : a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)
• Nat.ord_compl_mul 📋 Mathlib.Data.Nat.Factorization.Basic
  (a b p : ℕ) : a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)
• Nat.multiplicative_factorization 📋 Mathlib.Data.Nat.Factorization.Induction
  {β : Type u_1} [CommMonoid β] (f : ℕ → β) (h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y) (hf : f 1 = 1) {n : ℕ} : n ≠ 0 → f n = n.factorization.prod fun p k => f (p ^ k)
• Nat.multiplicative_factorization' 📋 Mathlib.Data.Nat.Factorization.Induction
  {n : ℕ} {β : Type u_1} [CommMonoid β] (f : ℕ → β) (h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y) (hf0 : f 0 = 1) (hf1 : f 1 = 1) : f n = n.factorization.prod fun p k => f (p ^ k)
• Nat.totient_eq_prod_factorization 📋 Mathlib.Data.Nat.Totient
  {n : ℕ} (hn : n ≠ 0) : n.totient = n.factorization.prod fun p k => p ^ (k - 1) * (p - 1)
• Nat.Prime.exists_addOrderOf_eq_pow_padic_val_nat_add_exponent 📋 Mathlib.GroupTheory.Exponent
  (G : Type u) [AddMonoid G] {p : ℕ} (hp : Nat.Prime p) : ∃ g, addOrderOf g = p ^ (AddMonoid.exponent G).factorization p
• Nat.Prime.exists_orderOf_eq_pow_factorization_exponent 📋 Mathlib.GroupTheory.Exponent
  (G : Type u) [Monoid G] {p : ℕ} (hp : Nat.Prime p) : ∃ g, orderOf g = p ^ (Monoid.exponent G).factorization p
• Sylow.ofCard 📋 Mathlib.GroupTheory.Sylow
  {G : Type u_1} [Group G] [Finite G] {p : ℕ} [Fact (Nat.Prime p)] (H : Subgroup G) (card_eq : Nat.card ↥H = p ^ (Nat.card G).factorization p) : Sylow p G
• Sylow.card_eq_multiplicity 📋 Mathlib.GroupTheory.Sylow
  {G : Type u} [Group G] [Finite G] {p : ℕ} [hp : Fact (Nat.Prime p)] (P : Sylow p G) : Nat.card ↥↑P = p ^ (Nat.card G).factorization p
• Sylow.coe_ofCard 📋 Mathlib.GroupTheory.Sylow
  {G : Type u_1} [Group G] [Finite G] {p : ℕ} [Fact (Nat.Prime p)] (H : Subgroup G) (card_eq : Nat.card ↥H = p ^ (Nat.card G).factorization p) : ↑(Sylow.ofCard H card_eq) = H
• Real.log_nat_eq_sum_factorization 📋 Mathlib.Analysis.SpecialFunctions.Log.Basic
  (n : ℕ) : Real.log ↑n = n.factorization.sum fun p t => ↑t * Real.log ↑p
• Real.logb_nat_eq_sum_factorization 📋 Mathlib.Analysis.SpecialFunctions.Log.Base
  {b : ℝ} (n : ℕ) : Real.logb b ↑n = n.factorization.sum fun p t => ↑t * Real.logb b ↑p
• IsPrimePow.factorization_minFac_ne_zero 📋 Mathlib.Data.Nat.Factorization.PrimePow
  {n : ℕ} (hn : IsPrimePow n) : n.factorization n.minFac ≠ 0
• isPrimePow_iff_factorization_eq_single 📋 Mathlib.Data.Nat.Factorization.PrimePow
  {n : ℕ} : IsPrimePow n ↔ ∃ p k, 0 < k ∧ n.factorization = fun₀ | p => k
• IsPrimePow.minFac_pow_factorization_eq 📋 Mathlib.Data.Nat.Factorization.PrimePow
  {n : ℕ} (hn : IsPrimePow n) : n.minFac ^ n.factorization n.minFac = n
• isPrimePow_of_minFac_pow_factorization_eq 📋 Mathlib.Data.Nat.Factorization.PrimePow
  {n : ℕ} (h : n.minFac ^ n.factorization n.minFac = n) (hn : n ≠ 1) : IsPrimePow n
• isPrimePow_iff_minFac_pow_factorization_eq 📋 Mathlib.Data.Nat.Factorization.PrimePow
  {n : ℕ} (hn : n ≠ 1) : IsPrimePow n ↔ n.minFac ^ n.factorization n.minFac = n
• IsPrimePow.exists_ordCompl_eq_one 📋 Mathlib.Data.Nat.Factorization.PrimePow
  {n : ℕ} (h : IsPrimePow n) : ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
• IsPrimePow.exists_ord_compl_eq_one 📋 Mathlib.Data.Nat.Factorization.PrimePow
  {n : ℕ} (h : IsPrimePow n) : ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
• exists_ordCompl_eq_one_iff_isPrimePow 📋 Mathlib.Data.Nat.Factorization.PrimePow
  {n : ℕ} (hn : n ≠ 1) : IsPrimePow n ↔ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
• exists_ord_compl_eq_one_iff_isPrimePow 📋 Mathlib.Data.Nat.Factorization.PrimePow
  {n : ℕ} (hn : n ≠ 1) : IsPrimePow n ↔ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
• Nat.Primes.prodNatEquiv_symm_apply 📋 Mathlib.Data.Nat.Factorization.PrimePow
  {n : ℕ} (hn : IsPrimePow n) : Nat.Primes.prodNatEquiv.symm ⟨n, hn⟩ = (⟨n.minFac, ⋯⟩, n.factorization n.minFac - 1)
• Squarefree.natFactorization_le_one 📋 Mathlib.Data.Nat.Squarefree
  {n : ℕ} (p : ℕ) (hn : Squarefree n) : n.factorization p ≤ 1
• Nat.factorization_eq_one_of_squarefree 📋 Mathlib.Data.Nat.Squarefree
  {n p : ℕ} (hn : Squarefree n) (hp : Nat.Prime p) (hpn : p ∣ n) : n.factorization p = 1
• Nat.squarefree_of_factorization_le_one 📋 Mathlib.Data.Nat.Squarefree
  {n : ℕ} (hn : n ≠ 0) (hn' : ∀ (p : ℕ), n.factorization p ≤ 1) : Squarefree n
• Nat.squarefree_iff_factorization_le_one 📋 Mathlib.Data.Nat.Squarefree
  {n : ℕ} (hn : n ≠ 0) : Squarefree n ↔ ∀ (p : ℕ), n.factorization p ≤ 1
• Nat.prod_primeFactors_invOn_squarefree 📋 Mathlib.Data.Nat.Squarefree
  : Set.InvOn (fun n => n.factorization.support) (fun s => ∏ p ∈ s, p) {s | ∀ p ∈ s, Nat.Prime p} {n | Squarefree n}
• Nat.card_divisors 📋 Mathlib.NumberTheory.ArithmeticFunction
  {n : ℕ} (hn : n ≠ 0) : n.divisors.card = ∏ x ∈ n.primeFactors, (n.factorization x + 1)
• Nat.sum_divisors 📋 Mathlib.NumberTheory.ArithmeticFunction
  {n : ℕ} (hn : n ≠ 0) : ∑ d ∈ n.divisors, d = ∏ p ∈ n.primeFactors, ∑ k ∈ Finset.range (n.factorization p + 1), p ^ k
• ArithmeticFunction.IsMultiplicative.multiplicative_factorization 📋 Mathlib.NumberTheory.ArithmeticFunction
  {R : Type u_1} [CommMonoidWithZero R] (f : ArithmeticFunction R) (hf : f.IsMultiplicative) {n : ℕ} (hn : n ≠ 0) : f n = n.factorization.prod fun p k => f (p ^ k)
• Nat.factorization_choose_le_log 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n k : ℕ} : (n.choose k).factorization p ≤ Nat.log p n
• Nat.factorization_factorial_eq_zero_of_lt 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n : ℕ} (h : n < p) : n.factorial.factorization p = 0
• Nat.factorization_choose_eq_zero_of_lt 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n k : ℕ} (h : n < p) : (n.choose k).factorization p = 0
• Nat.factorization_centralBinom_eq_zero_of_two_mul_lt 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n : ℕ} (h : 2 * n < p) : n.centralBinom.factorization p = 0
• Nat.le_two_mul_of_factorization_centralBinom_pos 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n : ℕ} (h_pos : 0 < n.centralBinom.factorization p) : p ≤ 2 * n
• Nat.pow_factorization_choose_le 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n k : ℕ} (hn : 0 < n) : p ^ (n.choose k).factorization p ≤ n
• Nat.factorization_choose_le_one 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n k : ℕ} (p_large : n < p ^ 2) : (n.choose k).factorization p ≤ 1
• Nat.prod_pow_factorization_choose 📋 Mathlib.Data.Nat.Choose.Factorization
  (n k : ℕ) (hkn : k ≤ n) : ∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p = n.choose k
• Nat.prod_pow_factorization_centralBinom 📋 Mathlib.Data.Nat.Choose.Factorization
  (n : ℕ) : ∏ p ∈ Finset.range (2 * n + 1), p ^ n.centralBinom.factorization p = n.centralBinom
• Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n : ℕ} (n_big : 2 < n) (p_le_n : p ≤ n) (big : 2 * n < 3 * p) : n.centralBinom.factorization p = 0
• Nat.factorization_choose_of_lt_three_mul 📋 Mathlib.Data.Nat.Choose.Factorization
  {p n k : ℕ} (hp' : p ≠ 2) (hk : p ≤ k) (hk' : p ≤ n - k) (hn : n < 3 * p) : (n.choose k).factorization p = 0
• Nat.factorization_ceilRoot 📋 Mathlib.Data.Nat.Factorization.Root
  (n a : ℕ) : (n.ceilRoot a).factorization = a.factorization ⌈/⌉ n
• Nat.factorization_floorRoot 📋 Mathlib.Data.Nat.Factorization.Root
  (n a : ℕ) : (n.floorRoot a).factorization = a.factorization ⌊/⌋ n
• Nat.floorRoot.eq_1 📋 Mathlib.Data.Nat.Factorization.Root
  (n a : ℕ) : n.floorRoot a = if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k => p ^ (k / n)
• Nat.ceilRoot.eq_1 📋 Mathlib.Data.Nat.Factorization.Root
  (n a : ℕ) : n.ceilRoot a = if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k => p ^ ((k + n - 1) / n)
• Nat.ceilRoot_def 📋 Mathlib.Data.Nat.Factorization.Root
  {a n : ℕ} : n.ceilRoot a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun x1 x2 => x1 ^ x2
• Nat.floorRoot_def 📋 Mathlib.Data.Nat.Factorization.Root
  {a n : ℕ} : n.floorRoot a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun x1 x2 => x1 ^ x2
• centralBinom_factorization_small 📋 Mathlib.NumberTheory.Bertrand
  (n : ℕ) (n_large : 2 < n) (no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n) : n.centralBinom = ∏ p ∈ Finset.range (2 * n / 3 + 1), p ^ n.centralBinom.factorization p

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, _ * _, _ ^ _, |- _ < _ → _
would 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 19971e9 serving mathlib revision e0654b0