Theorems · Theorem · number theory
Nat.primeFactorsList_count_eq
∀ {n p : ℕ}, List.count p n.primeFactorsList = n.factorization pWe can write both n.factorization p and n.factors.count p to represent the power
of p in the factorization of n: we declare the former to be the simp-normal form.
- Defined in
- Mathlib.Data.Nat.Factorization.Defs
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Finsuppstatement · cited by 5,255
- le_antisymmproof · cited by 2,068
- Nat.Primeproof · cited by 2,059
- le_rflproof · cited by 1,558
- LT.lt.ne'proof · cited by 1,417
- Nat.factorizationstatement and proof · cited by 215
- Nat.primeFactorsproof · cited by 129
- padicValNatproof · cited by 106
- Nat.primeFactorsListstatement and proof · cited by 105
- Nat.prime_of_mem_primeFactorsListproof · cited by 30
- lt_iff_not_geproof · cited by 22
Cited by11
Results whose statement or proof uses this declaration.
- Nat.ordProj_dvdproof · cited by 17
- Nat.Prime.factorizationproof · cited by 11
- Nat.eq_of_factorization_eqproof · cited by 7
- Nat.Prime.factorization_pos_of_dvdproof · cited by 3
- Nat.factorization_eq_primeFactorsList_multisetproof · cited by 2
- AddMonoid.exists_addOrderOf_eq_exponentproof · cited by 1
- Nat.factorization_eq_of_coprime_leftproof · cited by 1
- Nat.squarefree_of_factorization_le_oneproof · cited by 1
- Monoid.exists_orderOf_eq_exponentproof · cited by 1
- ArithmeticFunction.cardFactors_eq_sum_factorizationproof · cited by 0
- isPrimePow_iff_unique_prime_dvdproof · cited by 0