Documentation Verification Report

Carmichael

📁 Source: Mathlib/NumberTheory/ArithmeticFunction/Carmichael.lean

Statistics

Metric	Count
Definitions `Carmichael`, `«termλ»`	2
Theorems `carmichael_dvd`, `carmichael_dvd_totient`, `carmichael_eq_exponent`, `carmichael_eq_exponent'`, `carmichael_factorization`, `carmichael_finset_lcm`, `carmichael_finset_prod`, `carmichael_lcm`, `carmichael_mul`, `carmichael_pow_of_prime_ne_two`, `carmichael_two_pow_of_le_two`, `carmichael_two_pow_of_le_two_eq_totient`, `carmichael_two_pow_of_ne_two`, `pow_carmichael`, `two_mul_carmichael_two_pow_of_three_le_eq_totient`	15
Total	17

ArithmeticFunction

Definitions

Name	Category	Theorems
`Carmichael` 📖	CompOp	15 math math: `carmichael_pow_of_prime_ne_two`, `two_mul_carmichael_two_pow_of_three_le_eq_totient`, `pow_carmichael`, `carmichael_two_pow_of_le_two`, `carmichael_two_pow_of_le_two_eq_totient`, `carmichael_dvd`, `carmichael_finset_lcm`, `carmichael_dvd_totient`, `carmichael_finset_prod`, `carmichael_eq_exponent'`, `carmichael_eq_exponent`, `carmichael_mul`, `carmichael_factorization`, `carmichael_lcm`, `carmichael_two_pow_of_ne_two`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`carmichael_dvd` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `Carmichael`	—	`map_zero` `carmichael_eq_exponent` `ne_zero_of_dvd_ne_zero` `carmichael_eq_exponent'` `MonoidHom.exponent_dvd` `MonoidHom.instMonoidHomClass` `ZMod.unitsMap_surjective`
`carmichael_dvd_totient` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `Carmichael` `Nat.totient`	—	`map_zero` `ZMod.card_units_eq_totient` `carmichael_eq_exponent'` `Group.exponent_dvd_card`
`carmichael_eq_exponent` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `Carmichael` `Monoid.exponent` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `Units.instMonoid`	—	—
`carmichael_eq_exponent'` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `Carmichael` `Monoid.exponent` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `Units.instMonoid`	—	`carmichael_eq_exponent`
`carmichael_factorization` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `Carmichael` `Finset.lcm` `Nat.instCommMonoidWithZero` `instNormalizedGCDMonoidNat` `Nat.primeFactors` `Monoid.toNatPow` `Nat.instMonoid` `Finsupp` `Finsupp.instFunLike` `Nat.factorization`	—	`Nat.factorization_prod_pow_eq_self` `carmichael_finset_prod` `Pairwise.set_of_subtype` `Nat.pairwise_coprime_pow_primeFactors_factorization`
`carmichael_finset_lcm` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `Carmichael` `Finset.lcm` `Nat.instCommMonoidWithZero` `instNormalizedGCDMonoidNat`	—	`Finset.induction` `carmichael_eq_exponent'` `Monoid.exp_eq_one_of_subsingleton` `Unique.instSubsingleton` `Finset.lcm_insert` `carmichael_lcm`
`carmichael_finset_prod` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun`	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `Carmichael` `Finset.prod` `Nat.instCommMonoid` `Finset.lcm` `Nat.instCommMonoidWithZero` `instNormalizedGCDMonoidNat`	—	`carmichael_finset_lcm` `Finset.lcm_eq_prod`
`carmichael_lcm` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `Carmichael`	—	`dvd_antisymm` `Nat.instIsCancelMulZero` `Unique.instSubsingleton` `carmichael_eq_exponent` `lcm_eq_nat_lcm` `Monoid.exponent_prod` `Monoid.exponent_eq_of_mulEquiv` `Monoid.exponent_dvd_of_monoidHom` `dvd_refl` `Nat.lcm.charP` `ZMod.charP` `Units.map_injective` `ZMod.castHom_injective` `carmichael_dvd`
`carmichael_mul` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `Carmichael`	—	`carmichael_lcm` `Nat.Coprime.lcm_eq_mul`
`carmichael_pow_of_prime_ne_two` 📖	mathematical	`Nat.Prime`	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `Carmichael` `Monoid.toNatPow` `Nat.instMonoid` `Nat.totient`	—	`Nat.Prime.ne_zero` `carmichael_eq_exponent'` `ZMod.card_units_eq_totient` `Fintype.card_eq_nat_card` `IsCyclic.iff_exponent_eq_card` `instFiniteZModUnits` `ZMod.isCyclic_units_of_prime_pow`
`carmichael_two_pow_of_le_two` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `Carmichael` `Monoid.toNatPow` `Nat.instMonoid`	—	`carmichael_two_pow_of_le_two_eq_totient` `le_antisymm` `Mathlib.Tactic.IntervalCases.of_le_right` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_ofNat`
`carmichael_two_pow_of_le_two_eq_totient` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `Carmichael` `Monoid.toNatPow` `Nat.instMonoid` `Nat.totient`	—	`carmichael_eq_exponent'` `ZMod.card_units_eq_totient` `Fintype.card_eq_nat_card` `IsCyclic.iff_exponent_eq_card` `instFiniteZModUnits` `ZMod.isCyclic_units_two_pow_iff`
`carmichael_two_pow_of_ne_two` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `Carmichael` `Monoid.toNatPow` `Nat.instMonoid`	—	`carmichael_eq_exponent'` `dvd_antisymm` `Nat.instIsCancelMulZero` `Unique.instSubsingleton` `Nat.card_eq_fintype_card` `ZMod.card_units_eq_totient` `Nat.totient_prime_pow` `Nat.prime_two` `mul_one` `Nat.dvd_prime_pow` `Group.exponent_dvd_nat_card` `Iff.not` `IsCyclic.iff_exponent_eq_card` `instFiniteZModUnits` `ZMod.isCyclic_units_two_pow_iff` `Nat.instAtLeastTwoHAddOfNat` `ZMod.orderOf_five` `orderOf_units` `Monoid.order_dvd_exponent`
`pow_carmichael` 📖	mathematical	—	`Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `Monoid.toNatPow` `Units.instMonoid` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `Carmichael` `Units.instOne`	—	`map_zero` `pow_zero` `carmichael_eq_exponent'` `Monoid.pow_exponent_eq_one`
`two_mul_carmichael_two_pow_of_three_le_eq_totient` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `Carmichael` `Monoid.toNatPow` `Nat.instMonoid` `Nat.totient`	—	`carmichael_two_pow_of_ne_two` `Nat.totient_prime_pow` `Nat.prime_two`

ArithmeticFunction.Carmichael

Definitions

Name	Category	Theorems
`«termλ»` 📖	CompOp	—

---

← Back to Index