Totient

📁 Source: Mathlib/Data/Nat/Totient.lean

Statistics

Metric	Count
Definitions `evalNatTotient`, `termφ`, `totient`	3
Theorems `eq_of_totient_eq_totient`, `Ico_filter_coprime_le`, `card_units_zmod_lt_sub_one`, `dvd_two_of_totient_le_one`, `eq_or_eq_of_totient_eq_totient`, `filter_coprime_Ico_eq_totient`, `neZero_totient`, `odd_totient_iff`, `odd_totient_iff_eq_one`, `prime_iff_card_units`, `prime_pow_pow_totient_ediv_prod`, `prod_primeFactors_pow_totient_ediv_dvd`, `sum_totient`, `sum_totient'`, `totient_coprime_totient_iff`, `totient_div_of_dvd`, `totient_dvd_of_dvd`, `totient_eq_card_coprime`, `totient_eq_card_lt_and_coprime`, `totient_eq_div_primeFactors_mul`, `totient_eq_iff_prime`, `totient_eq_mul_prod_factors`, `totient_eq_one_iff`, `totient_eq_prod_factorization`, `totient_eq_zero`, `totient_even`, `totient_gcd_mul_totient_mul`, `totient_le`, `totient_lt`, `totient_mul`, `totient_mul_of_prime_of_dvd`, `totient_mul_of_prime_of_not_dvd`, `totient_mul_prod_primeFactors`, `totient_one`, `totient_pos`, `totient_prime`, `totient_prime_pow`, `totient_prime_pow_succ`, `totient_super_multiplicative`, `totient_two`, `totient_two_mul_of_even`, `totient_two_mul_of_odd`, `totient_zero`, `card_units_eq_totient`	44
Total	47

Even

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_totient_eq_totient` 📖	—	`Even` `Nat.totient`	—	—	`Nat.totient_eq_zero` `Nat.totient_zero` `Nat.eq_or_eq_of_totient_eq_totient` `Iff.not` `Nat.totient_mul_of_prime_of_dvd` `Nat.prime_two` `Nat.instAtLeastTwoHAddOfNat` `even_iff_two_dvd`

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalNatTotient` 📖	CompOp	—

Nat

Definitions

Name	Category	Theorems
`termφ` 📖	CompOp	—
`totient` 📖	CompOp	93 math math: `ArithmeticFunction.vonMangoldt.residueClass_eq`, `totient_dvd_of_dvd`, `IsPrimitiveRoot.totient_le_degree_minpoly`, `ArithmeticFunction.carmichael_pow_of_prime_ne_two`, `Polynomial.sub_one_pow_totient_le_cyclotomic_eval`, `odd_totient_iff`, `IsCyclotomicExtension.Rat.nrComplexPlaces_eq_totient_div_two`, `totient_mul_of_prime_of_not_dvd`, `Polynomial.cyclotomic_eval_lt_add_one_pow_totient`, `Polynomial.natDegree_cyclotomic`, `totient_eq_card_coprime`, `totient_prime_pow`, `IsCyclotomicExtension.Rat.discr_prime_pow'`, `totient_eq_mul_prod_factors`, `odd_totient_iff_eq_one`, `totient_coprime_totient_iff`, `IsCyclotomicExtension.Rat.absdiscr_prime_pow`, `ZMod.pow_totient`, `totient_le`, `sum_totient`, `DirichletCharacter.sum_characters_eq`, `ArithmeticFunction.vonMangoldt.residueClass_apply`, `totient_prime`, `Polynomial.sub_one_pow_totient_lt_natAbs_cyclotomic_eval`, `ArithmeticFunction.two_mul_carmichael_two_pow_of_three_le_eq_totient`, `ZMod.card_units_eq_totient`, `totient_div_of_dvd`, `totient_mul_of_prime_of_dvd`, `IsCyclotomicExtension.finrank`, `DirichletCharacter.sum_char_inv_mul_char_eq`, `IsPrimitiveRoot.power_basis_int'_dim`, `IsCyclotomicExtension.Rat.discr`, `totient_zero`, `IsPrimitiveRoot.integralPowerBasisOfPrimePow_dim`, `AddCircle.card_addOrderOf_eq_totient`, `ArithmeticFunction.carmichael_two_pow_of_le_two_eq_totient`, `totient_gcd_mul_totient_mul`, `IsCyclotomicExtension.Rat.discr_prime_pow_ne_two'`, `totient_mul`, `IsCyclotomicExtension.discr_prime_pow_ne_two`, `totient_two_mul_of_even`, `totient_eq_zero`, `ModEq.pow_totient`, `IsCyclic.card_mulAut`, `IsPrimitiveRoot.card_primitiveRoots`, `totient_two`, `sum_totient'`, `IsAddCyclic.card_addOrderOf_eq_totient`, `primeCounting'_add_le`, `IsCyclotomicExtension.Rat.natAbs_discr`, `Polynomial.natDegree_cyclotomic_le`, `totient_two_mul_of_odd`, `totient_eq_iff_prime`, `IsCyclic.card_orderOf_eq_totient`, `ArithmeticFunction.carmichael_dvd_totient`, `IsCyclotomicExtension.Rat.discr_prime_pow`, `Complex.card_primitiveRoots`, `Ico_filter_coprime_le`, `pow_totient_mod_eq_one`, `ArithmeticFunction.vonMangoldt.LSeries_residueClass_lower_bound`, `ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq`, `filter_coprime_Ico_eq_totient`, `neZero_totient`, `card_orderOf_eq_totient_aux₂`, `totient_eq_prod_factorization`, `Polynomial.degree_cyclotomic'`, `IsCyclotomicExtension.Rat.finrank`, `IsPrimitiveRoot.integralPowerBasis_dim`, `pow_add_mul_totient_mod_eq`, `card_addOrderOf_eq_totient_aux₂`, `Polynomial.cyclotomic_eval_le_add_one_pow_totient`, `DirichletCharacter.card_eq_totient_of_hasEnoughRootsOfUnity`, `totient_prime_pow_succ`, `totient_super_multiplicative`, `totient_lt`, `pow_totient_mod`, `Polynomial.sub_one_pow_totient_lt_cyclotomic_eval`, `pow_add_totient_mod_eq`, `Polynomial.natDegree_cyclotomic'`, `IsPrimitiveRoot.lcm_totient_le_finrank`, `totient_pos`, `totient_eq_card_lt_and_coprime`, `totient_eq_div_primeFactors_mul`, `ArithmeticFunction.vonMangoldt.eqOn_LFunctionResidueClassAux`, `Polynomial.degree_cyclotomic`, `Polynomial.normalizedFactors_cyclotomic_card`, `totient_eq_one_iff`, `totient_one`, `prime_pow_pow_totient_ediv_prod`, `prod_primeFactors_pow_totient_ediv_dvd`, `IsCyclotomicExtension.discr_prime_pow`, `totient_mul_prod_primeFactors`, `totient_even`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Ico_filter_coprime_le` 📖	mathematical	—	`Finset.card` `Finset.filter` `Finset.Ico` `instPreorder` `instLocallyFiniteOrder` `totient`	—	`filter_coprime_Ico_eq_totient` `Finset.filter.congr_simp` `MulZeroClass.mul_zero` `add_zero` `zero_add` `mul_one` `Finset.card_le_card` `Finset.filter_subset_filter` `Finset.Ico_subset_Ico` `le_refl` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `le_of_lt` `pos_iff_ne_zero` `instCanonicallyOrderedAdd` `Finset.Ico_subset_Ico_union_Ico` `Finset.filter_union` `Finset.card_union_le` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add`
`card_units_zmod_lt_sub_one` 📖	mathematical	—	`Fintype.card` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing`	—	`ZMod.card_units_eq_totient` `LT.lt.ne'` `pos_of_gt` `instCanonicallyOrderedAdd` `totient_lt`
`dvd_two_of_totient_le_one` 📖	—	`totient`	—	—	`totient_eq_one_iff` `le_antisymm` `totient_pos` `Mathlib.Meta.NormNum.isNat_dvd_true` `Mathlib.Meta.NormNum.isNat_ofNat`
`eq_or_eq_of_totient_eq_totient` 📖	—	`totient`	—	—	`totient_eq_zero` `totient_zero` `MulZeroClass.mul_zero` `coprime_of_dvd` `mul_comm` `lt_of_lt_of_le` `totient_mul_of_prime_of_dvd` `totient_pos` `pos_of_ne_zero` `instCanonicallyOrderedAdd` `Prime.one_lt` `mul_assoc` `totient_dvd_of_dvd` `Eq.not_lt` `totient_eq_one_iff` `Iff.not` `totient_mul` `mul_one`
`filter_coprime_Ico_eq_totient` 📖	mathematical	—	`Finset.card` `Finset.filter` `Finset.Ico` `instPreorder` `instLocallyFiniteOrder` `totient`	—	`totient.eq_1` `filter_Ico_card_eq_of_periodic` `periodic_coprime` `count_eq_card_filter_range`
`neZero_totient` 📖	mathematical	—	`MulZeroClass.toZero` `instMulZeroClass` `totient`	—	`LT.lt.ne'` `totient_pos` `NeZero.pos` `instCanonicallyOrderedAdd`
`odd_totient_iff` 📖	mathematical	—	`Odd` `instSemiring` `totient`	—	`instCharZero` `instAtLeastTwoHAddOfNat` `zero_add` `totient_two` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `instNoMaxOrder` `instCanonicallyOrderedAdd`
`odd_totient_iff_eq_one` 📖	mathematical	—	`Odd` `instSemiring` `totient`	—	—
`prime_iff_card_units` 📖	mathematical	—	`Prime` `Fintype.card` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing`	—	`eq_zero_or_neZero` `zero_tsub` `instCanonicallyOrderedAdd` `instOrderedSub` `instCharZero` `instAtLeastTwoHAddOfNat` `Fintype.card_congr'` `ZMod.card_units_eq_totient` `totient_eq_iff_prime` `NeZero.pos`
`prime_pow_pow_totient_ediv_prod` 📖	mathematical	`Prime`	`Monoid.toNatPow` `instMonoid` `totient` `Finset.prod` `instCommMonoid` `primeFactors`	—	`mul_left_comm` `le_mul_of_one_le_right` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `Right.one_le_mul` `covariant_swap_mul_of_covariant_mul` `instMulLeftMono` `Prime.one_lt` `totient_prime_pow` `Finset.prod_congr` `primeFactors_prime_pow` `LT.lt.ne'` `Finset.prod_singleton` `Prime.pos` `one_mul` `mul_one` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero`
`prod_primeFactors_pow_totient_ediv_dvd` 📖	mathematical	—	`Finset.prod` `instCommMonoid` `primeFactors` `Monoid.toNatPow` `instMonoid` `totient`	—	`prod_primeFactors_dvd` `dvd_trans` `Finset.prod_dvd_prod_of_dvd` `Finset.prod_pow` `LT.lt.ne'` `totient_pos`
`sum_totient` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid` `divisors` `totient`	—	`Finset.sum_congr` `divisors_zero` `sum_div_divisors` `Finset.card_range` `Finset.card_eq_sum_card_fiberwise` `mem_divisors` `LT.lt.ne'` `totient_div_of_dvd` `dvd_of_mem_divisors`
`sum_totient'` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid` `Finset.filter` `Finset.range` `totient`	—	`Finset.sum_congr` `Finset.filter.congr_simp` `Finset.range_eq_Ico` `Finset.sum_filter` `Finset.sum_eq_sum_Ico_succ_bot` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `instNoMaxOrder` `instCanonicallyOrderedAdd` `zero_add` `sum_totient`
`totient_coprime_totient_iff` 📖	mathematical	—	`totient`	—	`not_imp_not` `instAtLeastTwoHAddOfNat` `one_lt_two` `instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`totient_div_of_dvd` 📖	mathematical	—	`totient` `Finset.card` `Finset.filter` `Finset.range`	—	`eq_zero_of_zero_dvd` `Finset.filter.congr_simp` `Finset.filter_empty` `Finset.card_bij` `mul_lt_mul_of_pos_left` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `mul_one` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `LT.lt.ne'` `mul_lt_mul_iff_right₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE`
`totient_dvd_of_dvd` 📖	mathematical	—	`totient`	—	`eq_or_ne` `zero_dvd_iff` `primeFactors_mono` `totient_eq_prod_factorization` `Finsupp.prod_dvd_prod_of_subset_of_dvd` `mul_dvd_mul` `pow_dvd_pow` `tsub_le_tsub_right` `instOrderedSub` `factorization_le_iff_dvd` `dvd_rfl`
`totient_eq_card_coprime` 📖	mathematical	—	`totient` `Finset.card` `Finset.filter` `Finset.range`	—	—
`totient_eq_card_lt_and_coprime` 📖	mathematical	—	`totient` `card` `Set.Elem` `setOf`	—	`Subtype.coe_eta` `totient_eq_card_coprime` `card_congr` `card_eq_fintype_card` `Fintype.card_coe`
`totient_eq_div_primeFactors_mul` 📖	mathematical	—	`totient` `Finset.prod` `instCommMonoid` `primeFactors`	—	`Finset.prod_pos` `instZeroLEOneClass` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `instNontrivial` `pos_of_mem_primeFactors` `totient_mul_prod_primeFactors` `mul_comm` `prod_primeFactors_dvd`
`totient_eq_iff_prime` 📖	mathematical	—	`totient` `Prime`	—	`lt_of_le_of_ne` `one_ne_zero` `tsub_self` `instCanonicallyOrderedAdd` `instOrderedSub` `totient_one` `prime_of_coprime` `Finset.filter_card_eq` `card_Ico` `dvd_refl` `dvd_zero` `Finset.filter_insert` `Finset.insert_Ico_add_one_left_eq_Ico` `LT.lt.le` `Finset.range_eq_Ico` `totient_eq_card_coprime` `Finset.mem_Ico` `totient_prime`
`totient_eq_mul_prod_factors` 📖	mathematical	—	`totient` `Finset.prod` `Rat.commMonoid` `primeFactors`	—	`CharP.cast_eq_zero` `CharP.ofCharZero` `Rat.instCharZero` `Finset.prod_congr` `primeFactors_zero` `mul_one` `cast_prod` `cast_ne_zero` `zero_lt_iff` `prod_primeFactors_prod_factorization` `Finset.prod_pos` `instZeroLEOneClass` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `instNontrivial` `pos_of_mem_primeFactors` `totient_eq_div_primeFactors_mul` `cast_mul` `cast_div_charZero` `prod_primeFactors_dvd` `mul_comm_div` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `Rat.isDomain` `div_eq_iff` `pos_of_mem_primeFactorsList` `List.mem_toFinset` `LT.lt.ne` `sub_mul` `one_mul` `mul_comm` `mul_inv_cancel₀` `cast_pred`
`totient_eq_one_iff` 📖	mathematical	—	`totient`	—	`instCharZero` `instAtLeastTwoHAddOfNat` `totient_two` `le_add_self` `instCanonicallyOrderedAdd` `not_even_one` `totient_even`
`totient_eq_prod_factorization` 📖	mathematical	—	`totient` `Finsupp.prod` `MulZeroClass.toZero` `instMulZeroClass` `instCommMonoid` `factorization` `Monoid.toNatPow` `instMonoid`	—	`multiplicative_factorization` `totient_mul` `totient_one` `Finsupp.prod_congr` `zero_lt_iff` `Finsupp.mem_support_iff` `totient_prime_pow` `prime_of_mem_primeFactors`
`totient_eq_zero` 📖	mathematical	—	`totient`	—	`instNoMaxOrder`
`totient_even` 📖	mathematical	—	`Even` `totient`	—	`orderOf_units` `Units.coe_neg_one` `orderOf_neg_one` `ZMod.nontrivial` `LT.lt.trans` `instAtLeastTwoHAddOfNat` `one_lt_two` `instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `ringChar.eq` `ZMod.charP` `LT.lt.ne'` `NeZero.of_gt` `instCanonicallyOrderedAdd` `ZMod.card_units_eq_totient` `even_iff_two_dvd` `orderOf_dvd_card`
`totient_gcd_mul_totient_mul` 📖	mathematical	—	`totient`	—	`mul_mul_mul_comm` `totient_eq_div_primeFactors_mul` `prod_primeFactors_dvd` `prod_primeFactors_gcd_mul_prod_primeFactors_mul` `mul_comm` `mul_assoc` `mul_dvd_mul`
`totient_le` 📖	mathematical	—	`totient`	—	`LE.le.trans_eq` `Finset.card_filter_le` `Finset.card_range`
`totient_lt` 📖	mathematical	—	`totient`	—	`LT.lt.trans_eq` `Finset.card_lt_card` `Finset.filter_ssubset` `pos_of_gt` `instCanonicallyOrderedAdd` `LT.lt.ne'` `Finset.card_range`
`totient_mul` 📖	mathematical	—	`totient`	—	`MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `left_ne_zero_of_mul` `right_ne_zero_of_mul` `Fintype.card_congr` `Fintype.card_prod`
`totient_mul_of_prime_of_dvd` 📖	mathematical	`Prime`	`totient`	—	`totient_gcd_mul_totient_mul` `mul_comm` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `LT.lt.ne'` `totient_pos` `Prime.pos` `mul_assoc`
`totient_mul_of_prime_of_not_dvd` 📖	mathematical	`Prime`	`totient`	—	`totient_mul` `coprime_or_dvd_of_prime` `totient_prime`
`totient_mul_prod_primeFactors` 📖	mathematical	—	`totient` `Finset.prod` `instCommMonoid` `primeFactors`	—	`Finset.prod_congr` `primeFactors_zero` `mul_one` `totient_eq_prod_factorization` `factorization_prod_pow_eq_self` `Finsupp.prod_congr` `mul_comm` `mul_assoc` `zero_lt_iff` `Finsupp.mem_support_iff`
`totient_one` 📖	mathematical	—	`totient`	—	—
`totient_pos` 📖	mathematical	—	`totient`	—	`instCanonicallyOrderedAdd`
`totient_prime` 📖	mathematical	`Prime`	`totient`	—	`pow_one` `totient_prime_pow` `instZeroLEOneClass` `tsub_self` `instCanonicallyOrderedAdd` `instOrderedSub` `pow_zero` `one_mul`
`totient_prime_pow` 📖	mathematical	`Prime`	`totient` `Monoid.toNatPow` `instMonoid`	—	`pos_iff_ne_zero` `instCanonicallyOrderedAdd` `totient_prime_pow_succ`
`totient_prime_pow_succ` 📖	mathematical	`Prime`	`totient` `Monoid.toNatPow` `instMonoid`	—	`totient_eq_card_coprime` `Finset.sdiff_eq_filter` `Finset.filter_congr` `coprime_pow_left_iff` `Prime.coprime_iff_not_dvd` `dvd_mul_left` `lt_of_mul_lt_mul_left` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `mul_comm` `mul_left_injective₀` `IsCancelMulZero.toIsRightCancelMulZero` `instIsCancelMulZero` `Prime.ne_zero` `mul_lt_mul_iff_left₀` `IsStrictOrderedRing.toMulPosStrictMono` `instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `Prime.pos` `Finset.card_sdiff_of_subset` `Finset.card_image_of_injective` `Finset.card_range` `one_mul` `tsub_mul` `instCanonicallyOrderedAdd` `instOrderedSub` `LE.total` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `covariant_swap_mul_of_covariant_mul` `instMulLeftMono`
`totient_super_multiplicative` 📖	mathematical	—	`totient`	—	`LE.le.eq_or_lt` `MulZeroClass.zero_mul` `le_of_mul_le_mul_right` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `instIsStrictOrderedRing` `totient_gcd_mul_totient_mul` `mul_comm` `le_imp_le_of_le_of_le` `mul_le_mul_right` `instMulLeftMono` `totient_le` `le_refl`
`totient_two` 📖	mathematical	—	`totient`	—	`totient_prime` `prime_two`
`totient_two_mul_of_even` 📖	mathematical	`Even`	`totient`	—	`totient_mul_of_prime_of_dvd` `prime_two` `Even.two_dvd`
`totient_two_mul_of_odd` 📖	mathematical	`Odd` `instSemiring`	`totient`	—	`totient_mul_of_prime_of_not_dvd` `prime_two` `Odd.not_two_dvd_nat` `one_mul`
`totient_zero` 📖	mathematical	—	`totient`	—	—

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_units_eq_totient` 📖	mathematical	—	`Fintype.card` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `Nat.totient`	—	`Fintype.card_congr` `Fintype.card_subtype` `Finset.card_eq_sum_ones` `Finset.sum_filter` `Finset.filter.congr_simp`

---

← Back to Index