CyclotomicUnits

📁 Source: Mathlib/RingTheory/RootsOfUnity/CyclotomicUnits.lean

Statistics

Metric	Count
Definitions	0
Theorems associated_map_sub_one_map_sub_one, associated_pow_add_sub_sub_one, associated_pow_sub_one_pow_of_coprime, associated_sub_one_map_sub_one, associated_sub_one_pow_sub_one_of_coprime, geom_sum_isUnit, geom_sum_isUnit', ntRootsFinset_pairwise_associated_sub_one_sub_of_prime, pow_sub_one_eq_geom_sum_mul_geom_sum_inv_mul_pow_sub_one	9
Total	9

IsPrimitiveRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associated_map_sub_one_map_sub_one 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe AlgEquiv AlgEquiv.instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass autToPow_spec associated_pow_sub_one_pow_of_coprime ZMod.val_coe_unit_coprime
associated_pow_add_sub_sub_one 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Monoid.toNatPow	—	isUnit geom_sum_isUnit mul_assoc
associated_pow_sub_one_pow_of_coprime 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Monoid.toNatPow AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	associated_sub_one_pow_sub_one_of_coprime
associated_sub_one_map_sub_one 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne DFunLike.coe AlgEquiv AlgEquiv.instFunLike	—	map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass autToPow_spec associated_sub_one_pow_sub_one_of_coprime ZMod.val_coe_unit_coprime
associated_sub_one_pow_sub_one_of_coprime 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Monoid.toNatPow	—	associated_of_dvd_dvd IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero mul_geom_sum pow_one one_pow sub_self Nat.exists_mul_mod_eq_one_of_coprime pow_mul pow_mod_orderOf eq_orderOf
geom_sum_isUnit 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.range Monoid.toNatPow	—	associated_pow_sub_one_pow_of_coprime mul_right_injective₀ IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Units.isUnit
geom_sum_isUnit' 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.range Monoid.toNatPow	—	Finset.sum_congr Finset.sum_singleton pow_zero one_pow Finset.sum_const Finset.card_range nsmul_eq_mul mul_one geom_sum_isUnit le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing Mathlib.Tactic.Linarith.natCast_nonneg Nat.cast_add
ntRootsFinset_pairwise_associated_sub_one_sub_of_prime 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid Nat.Prime	Set.Pairwise SetLike.coe Finset Finset.instSetLike Polynomial.nthRootsFinset AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	—	Nat.Prime.ne_zero eq_pow_of_pow_eq_one Polynomial.mem_nthRootsFinset Nat.Prime.pos Nat.coprime_of_lt_prime associated_pow_add_sub_sub_one Nat.Prime.two_le add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub associated_mul_unit_right_iff Associated.refl neg_sub Associated.neg_right
pow_sub_one_eq_geom_sum_mul_geom_sum_inv_mul_pow_sub_one 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units.val IsUnit.unit Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.range geom_sum_isUnit Units Units.instInv	—	—

---

← Back to Index