Documentation Verification Report

Three

📁 Source: Mathlib/NumberTheory/NumberField/Cyclotomic/Three.lean

Statistics

Metric	Count
Definitions	0
Theorems `mem`, `coe_eta`, `cube_sub_one_eq_mul`, `eq_one_or_neg_one_of_unit_of_congruent`, `eta_sq`, `eta_sq_add_eta_add_one`, `lambda_dvd_mul_sub_one_mul_sub_eta_add_one`, `lambda_dvd_or_dvd_sub_one_or_dvd_add_one`, `lambda_pow_four_dvd_cube_add_one_of_dvd_add_one`, `lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one`, `lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd`, `toInteger_cube_eq_one`	12
Total	12

IsCyclotomicExtension.Rat.Three

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_eta` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Units.val` `NumberField.RingOfIntegers` `CommMonoid.toMonoid` `NumberField.RingOfIntegers.instCommRing` `IsUnit.unit` `IsPrimitiveRoot.toInteger` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot`	—	`IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot`
`cube_sub_one_eq_mul` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`NumberField.RingOfIntegers` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `NumberField.RingOfIntegers.instCommRing` `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` `CommMonoid.toMonoid` `IsUnit.unit` `IsPrimitiveRoot.toInteger` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot`	—	`IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `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.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_congr` `IsPrimitiveRoot.toInteger_cube_eq_one` `eta_sq_add_eta_add_one` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero`
`eq_one_or_neg_one_of_unit_of_congruent` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Units.val` `AddGroupWithOne.toIntCast`	`Units` `Units.instOne` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing`	—	`NumberField.to_charZero` `Nat.instAtLeastTwoHAddOfNat` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `mul_assoc` `mul_neg` `neg_mul` `Units.mem` `IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two'` `Nat.fact_prime_three` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `sub_eq_iff_eq_add` `NegMemClass.neg_mem` `SubringClass.toNegMemClass` `Subalgebra.instSubringClass` `neg_neg` `Int.cast_neg` `IsPrimitiveRoot.pow_of_coprime` `NumberField.RingOfIntegers.ext` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`eta_sq` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`NumberField.RingOfIntegers` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Units.val` `CommMonoid.toMonoid` `IsUnit.unit` `IsPrimitiveRoot.toInteger` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `neg_add'` `add_eq_zero_iff_eq_neg` `add_assoc` `NumberField.RingOfIntegers.ext` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_one` `MonoidHomClass.toOneHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `Polynomial.cyclotomic_three` `Polynomial.eval_add` `Polynomial.eval_pow` `Polynomial.eval_X` `Polynomial.eval_one` `IsPrimitiveRoot.isRoot_cyclotomic` `instIsDomain`
`eta_sq_add_eta_add_one` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`NumberField.RingOfIntegers` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Units.val` `CommMonoid.toMonoid` `IsUnit.unit` `IsPrimitiveRoot.toInteger` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `eta_sq` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `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.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero`
`lambda_dvd_mul_sub_one_mul_sub_eta_add_one` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `Distrib.toAdd` `Units.val` `CommMonoid.toMonoid` `IsUnit.unit` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot`	—	`NumberField.to_charZero` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `lambda_dvd_or_dvd_sub_one_or_dvd_add_one` `dvd_mul_of_dvd_left` `dvd_mul_of_dvd_right` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.sub_pf` `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_mul` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `dvd_sub` `dvd_add` `Distrib.leftDistribClass` `dvd_rfl` `IsPrimitiveRoot.toInteger_sub_one_dvd_prime'` `Nat.fact_prime_three`
`lambda_dvd_or_dvd_sub_one_or_dvd_add_one` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing`	—	`NumberField.to_charZero` `NeZero.of_gt` `Nat.instCanonicallyOrderedAdd` `IsPrimitiveRoot.finite_quotient_toInteger_sub_one` `Ideal.instIsTwoSided_1` `Finset.mem_univ` `Nat.card_eq_fintype_card` `IsPrimitiveRoot.card_quotient_toInteger_sub_one` `NeZero.of_gt'` `Nat.Prime.one_lt'` `Nat.fact_prime_three` `IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two'` `Finset.univ_of_card_le_three` `Eq.le` `Ideal.mem_span_singleton` `Ideal.Quotient.eq_zero_iff_mem` `RingHom.map_sub` `RingHom.map_one` `sub_self` `RingHom.map_add` `neg_add_cancel`
`lambda_pow_four_dvd_cube_add_one_of_dvd_add_one` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`NumberField.to_charZero` `neg_add'` `Dvd.dvd.neg_right` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `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` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `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.Meta.NormNum.isInt_pow` `Mathlib.Meta.NormNum.intPow_negOfNat_bit1` `Mathlib.Meta.NormNum.one_natPow` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one`
`lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`NumberField.to_charZero` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `cube_sub_one_eq_mul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `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.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.pow_nat` `Mathlib.Tactic.Ring.coeff_one` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_bit1` `Mathlib.Tactic.Ring.pow_one` `pow_succ` `mul_dvd_mul_left` `lambda_dvd_mul_sub_one_mul_sub_eta_add_one`
`lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NumberField.RingOfIntegers` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `NumberField.RingOfIntegers.instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsPrimitiveRoot.toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing`	—	`NumberField.to_charZero` `lambda_dvd_or_dvd_sub_one_or_dvd_add_one` `lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one` `lambda_pow_four_dvd_cube_add_one_of_dvd_add_one`

IsCyclotomicExtension.Rat.Three.Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Units` `NumberField.RingOfIntegers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `CommMonoid.toMonoid` `Units.instOne` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsUnit.unit` `IsPrimitiveRoot.toInteger` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `Monoid.toNatPow` `Units.instMonoid`	—	`NumberField.to_charZero` `NumberField.InfinitePlace.card_eq_nrRealPlaces_add_nrComplexPlaces` `IsCyclotomicExtension.numberField` `Rat.numberField` `Finite.of_fintype` `IsCyclotomicExtension.Rat.nrRealPlaces_eq_zero` `zero_add` `IsCyclotomicExtension.Rat.nrComplexPlaces_eq_totient_div_two` `IsPrimitiveRoot.isUnit` `IsPrimitiveRoot.toInteger_isPrimitiveRoot` `NumberField.Units.exist_unique_eq_mul_prod` `mul_one` `Finset.prod_empty` `Finset.univ_eq_empty_iff` `Fin.isEmpty'` `isOfFinOrder_iff_pow_eq_one` `CommGroup.mem_torsion` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Nat.cast_one` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `SubmonoidClass.toOneMemClass` `map_one` `MonoidHomClass.toOneHomClass` `IsPrimitiveRoot.exists_pow_or_neg_mul_pow_of_isOfFinOrder` `Finset.mem_Ico` `Nat.instCanonicallyOrderedAdd` `Units.ext` `NumberField.RingOfIntegers.ext` `pow_zero` `NumberField.RingOfIntegers.instCharZero_1` `pow_one`

IsPrimitiveRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toInteger_cube_eq_one` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`NumberField.RingOfIntegers` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `toInteger` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`pow_eq_one` `toInteger_isPrimitiveRoot`

---

← Back to Index