Lemmas

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

Statistics

Metric	Count
Definitions	0
Theorems prod_one_sub_pow_eq_order, prod_pow_sub_one_eq_order, self_sub_one_pow_dvd_order	3
Total	3

IsPrimitiveRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_one_sub_pow_eq_order 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Finset.prod Finset.range SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toNatCast	—	X_pow_sub_C_eq_prod one_pow mul_right_cancel₀ Polynomial.instIsRightCancelMulZeroOfIsCancelAdd AddCancelMonoid.toIsCancelAdd IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Polynomial.X_sub_C_ne_zero IsDomain.toNontrivial mul_comm mul_one pow_zero Finset.prod_range_succ' mul_geom_sum Polynomial.C_1 Finset.prod_congr map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Polynomial.eval_prod Polynomial.eval_sub Polynomial.eval_X Polynomial.eval_pow Polynomial.eval_C Polynomial.eval_geom_sum Finset.sum_congr Finset.sum_const Finset.card_range nsmul_eq_mul Nat.cast_add Nat.cast_one
prod_pow_sub_one_eq_order 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Finset.prod Finset.range SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Distrib.toAdd AddMonoidWithOne.toNatCast	—	Finset.prod_const Finset.card_range Finset.prod_congr neg_one_mul neg_sub prod_one_sub_pow_eq_order
self_sub_one_pow_dvd_order 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Subalgebra Int.instCommSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toIntAlgebra CommRing.toRing SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AddMonoidWithOne.toOne	—	Subalgebra.sum_mem Subalgebra.pow_mem Algebra.self_mem_adjoin_singleton geom_sum_mul Subalgebra.mul_mem Subalgebra.neg_mem Subalgebra.one_mem Subalgebra.prod_mem Subalgebra.sub_mem Nat.cast_add Nat.cast_one prod_pow_sub_one_eq_order mul_assoc Finset.card_range Finset.prod_range_mul_prod_Ico mul_comm Finset.prod_mul_pow_card

---

← Back to Index