Theorems · Definition · number theory
ArithmeticFunction.carmichael
ArithmeticFunction ℕ
λ is the Carmichael function, also known as the reduced totient function,
defined as the exponent of the unit group of ZMod n.
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ArithmeticFunctionstatement · cited by 290
- Nat.findproof · cited by 139
Cited by17
Results whose statement or proof uses this declaration.
- ArithmeticFunction.carmichael_eq_exponent'statement · cited by 7
- ArithmeticFunction.carmichael_eq_exponentstatement · cited by 3
- ArithmeticFunction.carmichael_finsetProdstatement · cited by 2
- ArithmeticFunction.carmichael_lcmstatement and proof · cited by 2
- ArithmeticFunction.carmichael_dvdstatement and proof · cited by 1
- ArithmeticFunction.carmichael_finset_lcmstatement and proof · cited by 1
- ArithmeticFunction.carmichael_two_pow_of_le_two_eq_totientstatement · cited by 1
- ArithmeticFunction.carmichael_two_pow_of_ne_twostatement · cited by 1
- ArithmeticFunction.two_mul_carmichael_two_pow_of_three_le_eq_totientstatement · cited by 0
- ArithmeticFunction.carmichael_dvd_totientstatement and proof · cited by 0
- ArithmeticFunction.carmichael_factorizationstatement and proof · cited by 0
- ArithmeticFunction.carmichael_finset_prodstatement · cited by 0