Theorems · Theorem · number theory
ArithmeticFunction.carmichael_factorization
∀ (n : ℕ) [NeZero n], ArithmeticFunction.carmichael n = n.primeFactors.lcm fun p => ArithmeticFunction.carmichael (p ^ n.factorization p)
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NeZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
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
- SetLike.coeproof · cited by 8,199
- Finsuppstatement · cited by 5,255
- Finsupp.supportproof · cited by 828
- Function.onFunproof · cited by 570
- ArithmeticFunctionstatement · cited by 290
- Nat.factorizationstatement and proof · cited by 215
- Nat.primeFactorsstatement and proof · cited by 129
- Finset.lcmstatement and proof · cited by 37
- Nat.prod_factorization_pow_eq_selfproof · cited by 22
- ArithmeticFunction.carmichaelstatement and proof · cited by 16
- Pairwise.set_of_subtypeproof · cited by 4
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.