UnitsCyclic

📁 Source: Mathlib/RingTheory/ZMod/UnitsCyclic.lean

Statistics

Metric	Count
Definitions	0
Theorems `exists_one_add_mul_pow_prime_eq`, `exists_one_add_mul_pow_prime_pow_eq`, `isCyclic_units_four`, `isCyclic_units_four_mul_iff`, `isCyclic_units_iff`, `isCyclic_units_iff_of_odd`, `isCyclic_units_of_prime_pow`, `isCyclic_units_one`, `isCyclic_units_prime`, `isCyclic_units_two`, `isCyclic_units_two_mul_iff_of_odd`, `isCyclic_units_two_pow_iff`, `isCyclic_units_zero`, `not_isCyclic_units_eight`, `not_isCyclic_units_of_mul_coprime`, `orderOf_five`, `orderOf_one_add_four_mul`, `orderOf_one_add_mul_prime`, `orderOf_one_add_mul_prime_pow`, `orderOf_one_add_prime`	20
Total	20

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_one_add_mul_pow_prime_eq` 📖	mathematical	`Nat.Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`Distrib.toAdd` `AddMonoidWithOne.toOne`	—	`add_comm` `add_pow` `Finset.add_sum_erase` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `Nat.instCanonicallyOrderedAdd` `one_pow` `Finset.sum_congr` `pow_zero` `Nat.choose_zero_right` `Nat.cast_one` `mul_one` `Nat.Prime.pos` `Finset.sum_erase_add` `Nat.two_le_iff` `Nat.Prime.two_le` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Nat.instZeroLEOneClass` `mul_add` `Distrib.leftDistribClass` `Nat.choose_one_right` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_zero` `Finset.mul_sum` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero` `Nat.Prime.dvd_choose_self` `Nat.cast_mul` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `mul_pow` `Nat.choose_self`
`exists_one_add_mul_pow_prime_pow_eq` 📖	mathematical	`Nat.Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`Distrib.toAdd` `AddMonoidWithOne.toOne` `Nat.instMonoid`	—	`pow_zero` `pow_one` `one_mul` `MulZeroClass.mul_zero` `add_zero` `pow_succ'` `pow_mul` `exists_one_add_mul_pow_prime_eq` `mul_dvd_mul_left` `mul_pow` `mul_assoc` `mul_comm` `mul_dvd_mul` `pow_two` `pow_dvd_pow` `Nat.Prime.two_le` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `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.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.pow_one_cast`
`isCyclic_units_four` 📖	mathematical	—	`IsCyclic` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `DivInvMonoid.toZPow` `Units.instDivInvMonoid`	—	`isCyclic_of_prime_card` `Nat.fact_prime_two` `Nat.card_eq_fintype_card` `card_units_eq_totient`
`isCyclic_units_four_mul_iff` 📖	mathematical	—	`IsCyclic` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `DivInvMonoid.toZPow` `Units.instDivInvMonoid`	—	`eq_or_ne` `em` `mul_assoc` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `isCyclic_of_surjective` `MonoidHom.instMonoidHomClass` `dvd_mul_right` `unitsMap_surjective` `not_isCyclic_units_eight` `Nat.Prime.coprime_iff_not_dvd` `Nat.prime_two` `MulEquiv.isCyclic` `Group.isCyclic_prod_iff` `Nat.card_eq_fintype_card` `card_units_eq_totient` `Nat.odd_totient_iff`
`isCyclic_units_iff` 📖	mathematical	—	`IsCyclic` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `DivInvMonoid.toZPow` `Units.instDivInvMonoid` `Nat.Prime` `Odd` `Nat.instSemiring` `Monoid.toNatPow` `Nat.instMonoid`	—	`Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `Nat.instIsMulTorsionFree` `Nat.even_or_odd` `isCyclic_units_iff_of_odd` `Distrib.rightDistribClass` `Mathlib.Tactic.Contrapose.contrapose₂` `pow_zero` `Even.two_dvd` `isCyclic_units_two_mul_iff_of_odd` `Odd.pow` `zero_lt_two` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `mul_one` `mul_assoc` `isCyclic_units_four_mul_iff`
`isCyclic_units_iff_of_odd` 📖	mathematical	`Odd` `Nat.instSemiring`	`IsCyclic` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `DivInvMonoid.toZPow` `Units.instDivInvMonoid` `Nat.Prime` `Monoid.toNatPow` `Nat.instMonoid`	—	`Nat.not_odd_zero` `eq_or_ne` `Nat.prime_three` `pow_zero` `Nat.exists_prime_and_dvd` `Odd.of_dvd_nat` `isCyclic_units_of_prime_pow` `Odd.ne_two_of_dvd_nat` `dvd_rfl` `Nat.ordProj_dvd` `not_isCyclic_units_of_mul_coprime` `Nat.instIsMulTorsionFree` `LT.lt.ne'` `Nat.Prime.factorization_pos_of_dvd` `Nat.Prime.ne_one` `Mathlib.Tactic.Contrapose.contrapose₄` `one_mul` `Nat.coprime_ordCompl` `Nat.prime_dvd_prime_iff_eq` `Nat.Prime.dvd_of_dvd_pow` `Nat.factorization_pow` `Nat.Prime.factorization_self` `mul_one`
`isCyclic_units_of_prime_pow` 📖	mathematical	`Nat.Prime`	`IsCyclic` `Units` `ZMod` `Monoid.toNatPow` `Nat.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `DivInvMonoid.toZPow` `Units.instDivInvMonoid`	—	`pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `Nat.Prime.ne_zero` `pow_zero` `isCyclic_of_subsingleton` `Unique.instSubsingleton` `Nat.cast_one` `Nat.cast_add` `isUnit_iff_coprime` `orderOf_injective` `Units.coeHom_injective` `Units.coeHom_apply` `IsUnit.unit_spec` `orderOf_one_add_prime` `isCyclic_iff_exists_orderOf_eq_natCard` `instFiniteZModUnits` `isCyclic_units_prime` `Dvd.intro_left` `unitsMap_surjective` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `orderOf_map_dvd` `orderOf_pow_orderOf_div` `LT.lt.ne'` `orderOf_pos` `Commute.orderOf_mul_eq_mul_orderOf_of_coprime` `Commute.all` `Nat.coprime_self_sub_right` `Nat.Prime.pos` `zero_add` `Nat.card_eq_fintype_card` `card_units_eq_totient` `Nat.totient_prime_pow_succ` `card_units`
`isCyclic_units_one` 📖	mathematical	—	`IsCyclic` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `DivInvMonoid.toZPow` `Units.instDivInvMonoid`	—	`isCyclic_of_subsingleton` `Unique.instSubsingleton`
`isCyclic_units_prime` 📖	mathematical	`Nat.Prime`	`IsCyclic` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `DivInvMonoid.toZPow` `Units.instDivInvMonoid`	—	`instIsCyclicUnitsOfFinite` `instIsDomain` `instFiniteZModUnits`
`isCyclic_units_two` 📖	mathematical	—	`IsCyclic` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `Nat.fact_prime_two` `DivInvMonoid.toZPow` `Units.instDivInvMonoid`	—	`Nat.fact_prime_two` `instIsCyclicUnitsOfFinite` `instIsDomain` `instFiniteZModUnits`
`isCyclic_units_two_mul_iff_of_odd` 📖	mathematical	`Odd` `Nat.instSemiring`	`IsCyclic` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `DivInvMonoid.toZPow` `Units.instDivInvMonoid`	—	`Nat.fact_prime_two` `MulEquiv.isCyclic` `Nat.coprime_two_left` `Nat.card_eq_fintype_card` `card_units_eq_totient` `Nat.totient_two`
`isCyclic_units_two_pow_iff` 📖	mathematical	—	`IsCyclic` `Units` `ZMod` `Monoid.toNatPow` `Nat.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `DivInvMonoid.toZPow` `Units.instDivInvMonoid`	—	`Nat.instCanonicallyOrderedAdd` `isCyclic_units_prime` `Nat.prime_two` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instZeroLEOneClass` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `not_isCyclic_units_eight` `pow_dvd_pow` `isCyclic_of_surjective` `MonoidHom.instMonoidHomClass` `unitsMap_surjective`
`isCyclic_units_zero` 📖	mathematical	—	`IsCyclic` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `DivInvMonoid.toZPow` `Units.instDivInvMonoid`	—	`instIsCyclicUnitsOfFinite` `instIsDomainOfNatNat` `instFiniteZModUnits`
`not_isCyclic_units_eight` 📖	mathematical	—	`IsCyclic` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `DivInvMonoid.toZPow` `Units.instDivInvMonoid`	—	`IsCyclic.iff_exponent_eq_card` `instFiniteZModUnits` `Nat.card_eq_fintype_card` `card_units_eq_totient` `Monoid.exponent_dvd_of_forall_pow_eq_one`
`not_isCyclic_units_of_mul_coprime` 📖	mathematical	`Odd` `Nat.instSemiring`	`IsCyclic` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `DivInvMonoid.toZPow` `Units.instDivInvMonoid`	—	`Nat.ne_of_odd_add` `MulEquiv.isCyclic` `Group.isCyclic_prod_iff` `card_units_eq_totient` `Nat.card_eq_fintype_card`
`orderOf_five` 📖	mathematical	—	`orderOf` `ZMod` `Monoid.toNatPow` `Nat.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNat_add` `Nat.cast_one` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_intCast` `orderOf_one_add_four_mul`
`orderOf_one_add_four_mul` 📖	mathematical	`Odd` `Int.instSemiring`	`orderOf` `ZMod` `Monoid.toNatPow` `Nat.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Distrib.toMul` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat` `AddGroupWithOne.toIntCast`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `orderOf_one_add_mul_prime_pow` `Nat.prime_two` `two_ne_zero` `le_rfl` `even_iff_two_dvd` `Int.not_even_iff_odd`
`orderOf_one_add_mul_prime` 📖	mathematical	`Nat.Prime`	`orderOf` `ZMod` `Monoid.toNatPow` `Nat.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toIntCast`	—	`pow_one` `orderOf_one_add_mul_prime_pow` `one_ne_zero` `Nat.Prime.two_le`
`orderOf_one_add_mul_prime_pow` 📖	mathematical	`Nat.Prime`	`orderOf` `ZMod` `Monoid.toNatPow` `Nat.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toIntCast`	—	`Nat.cast_pow` `zero_add` `natCast_self` `MulZeroClass.zero_mul` `add_zero` `orderOf_one` `pow_zero` `exists_one_add_mul_pow_prime_pow_eq` `dvd_pow_self` `pow_succ'` `pow_succ` `pow_mul` `mul_comm` `pow_dvd_pow` `orderOf_eq_prime_pow` `pow_add` `add_eq_left` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `mul_add` `Distrib.leftDistribClass` `mul_assoc` `add_right_comm` `Int.cast_natCast` `Int.cast_mul` `intCast_zmod_eq_zero_iff_dvd` `Nat.cast_mul` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `Int.instNormMulClass` `Int.instNontrivial` `Nat.Prime.ne_zero` `CharP.cast_eq_zero` `charP`
`orderOf_one_add_prime` 📖	mathematical	`Nat.Prime`	`orderOf` `ZMod` `Monoid.toNatPow` `Nat.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toNatCast`	—	`Int.cast_one` `mul_one` `orderOf_one_add_mul_prime` `Nat.Prime.ne_one` `Int.instCharZero`

---

← Back to Index