Documentation Verification Report

Carmichael

πŸ“ Source: Mathlib/NumberTheory/ArithmeticFunction/Carmichael.lean

Statistics

MetricCount
DefinitionsCarmichael, «termλ»
2
Theoremscarmichael_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
Total17

ArithmeticFunction

Definitions

NameCategoryTheorems
Carmichael πŸ“–CompOp
15 mathmath: 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

NameKindAssumesProvesValidatesDepends 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 πŸ“–mathematicalSet.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 πŸ“–mathematicalNat.PrimeDFunLike.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

NameCategoryTheorems
Β«termλ» πŸ“–CompOpβ€”

---

← Back to Index