Documentation Verification Report

Discriminant

📁 Source: Mathlib/NumberTheory/Cyclotomic/Discriminant.lean

Statistics

Metric	Count
Definitions	0
Theorems `discr_odd_prime`, `discr_prime_pow`, `discr_prime_pow_eq_unit_mul_pow`, `discr_prime_pow_ne_two`, `discr_prime_pow_ne_two'`, `discr_zeta_eq_discr_zeta_sub_one`	6
Total	6

IsCyclotomicExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`discr_odd_prime` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`Algebra.discr` `PowerBasis.dim` `CommRing.toRing` `IsPrimitiveRoot.powerBasis` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `instIsDomain` `Field.toSemifield` `Fin.fintype` `DFunLike.coe` `Module.Basis` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Module.Basis.instFunLike` `PowerBasis.basis` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toNatCast`	—	`zero_add` `pow_one` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `instIsDomain` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable` `Fintype.instFastSubsingleton` `Nat.totient_prime` `Fact.out` `pow_zero` `one_mul` `mul_one` `discr_prime_pow_ne_two`
`discr_prime_pow` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`Algebra.discr` `PowerBasis.dim` `CommRing.toRing` `IsPrimitiveRoot.powerBasis` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `instIsDomain` `Field.toSemifield` `Fin.fintype` `DFunLike.coe` `Module.Basis` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Module.Basis.instFunLike` `PowerBasis.basis` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.totient` `AddMonoidWithOne.toNatCast`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `instIsDomain` `Matrix.det.congr_simp` `PowerBasis.coe_basis` `pow_zero` `IsPrimitiveRoot.powerBasis.congr_simp` `IsPrimitiveRoot.powerBasis_gen` `MulZeroClass.mul_zero` `IsPrimitiveRoot.powerBasis_dim` `RingHom.map_one` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.natDegree_X_sub_C` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_pow` `mul_one` `Matrix.det_unique` `Algebra.trace_algebraMap` `commRing_strongRankCondition` `Module.Free.of_divisionRing` `finrank` `one_smul` `zero_tsub` `Nat.instOrderedSub` `Nat.pow_right_injective` `Eq.le` `pow_one` `IsPrimitiveRoot.eq_neg_one_of_two_right` `IsDomain.to_noZeroDivisors` `map_neg` `RingHomClass.toAddMonoidHomClass` `FaithfulSMul.algebraMap_injective` `instFaithfulSMul_1` `Fin.equiv_iff_eq` `Algebra.discr_reindex` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.natPow_one` `Nat.totient_two` `Mathlib.Meta.NormNum.isNat_natDiv` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_natSub` `Mathlib.Meta.NormNum.natPow_zero` `Nat.cast_one` `Algebra.discr.congr_simp` `zero_add` `add_eq_right` `AddRightCancelSemigroup.toIsRightCancelAdd` `eq_of_prime_pow_eq` `Nat.instIsCancelMulZero` `Unique.instSubsingleton` `Nat.prime_iff` `Fact.out` `Nat.prime_two` `discr_prime_pow_ne_two`
`discr_prime_pow_eq_unit_mul_pow` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`Algebra.discr` `PowerBasis.dim` `CommRing.toRing` `IsPrimitiveRoot.powerBasis` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `instIsDomain` `Field.toSemifield` `Fin.fintype` `DFunLike.coe` `Module.Basis` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Module.Basis.instFunLike` `PowerBasis.basis` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `Units.val` `Int.instMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `instIsDomain` `discr_prime_pow` `Even.neg_one_pow` `one_mul` `Int.cast_one` `Odd.neg_one_pow` `Nat.not_even_iff_odd` `neg_mul` `Int.cast_neg`
`discr_prime_pow_ne_two` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`Algebra.discr` `PowerBasis.dim` `CommRing.toRing` `IsPrimitiveRoot.powerBasis` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `instIsDomain` `Field.toSemifield` `Fin.fintype` `DFunLike.coe` `Module.Basis` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Module.Basis.instFunLike` `PowerBasis.basis` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.totient` `AddMonoidWithOne.toNatCast`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `instIsDomain` `Algebra.discr_powerBasis_eq_norm` `finiteDimensional` `Finite.of_fintype` `isSeparable` `finrank` `IsPrimitiveRoot.powerBasis_gen` `IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible` `neZero'` `Nat.totient_prime_pow` `Fact.out` `eq_or_ne` `tsub_zero` `Nat.instOrderedSub` `mul_one` `pow_succ'` `mul_assoc` `Nat.instAtLeastTwoHAddOfNat` `zero_lt_two` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `pow_zero` `pow_one` `Even.neg_one_pow` `Even.mul_right` `Distrib.rightDistribClass` `even_two` `Nat.Prime.odd_of_ne_two` `Even.two_dvd` `Nat.Prime.even_sub_one` `mul_left_comm` `two_pos` `mul_right_comm` `pow_mul` `Odd.neg_one_pow` `Odd.mul` `Odd.pow` `Nat.Even.sub_odd` `one_le_mul` `Nat.instMulLeftMono` `Nat.Prime.pos` `tsub_pos_of_lt` `Nat.Prime.one_lt` `even_two_mul` `odd_one` `Polynomial.cyclotomic_prime_pow_mul_X_pow_sub_one` `Polynomial.C_eq_natCast` `Polynomial.derivative_X_pow` `sub_zero` `Polynomial.derivative_one` `Polynomial.derivative_sub` `Polynomial.derivative_mul` `Polynomial.aeval_add` `Polynomial.aeval_mul` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Polynomial.aeval_X_pow` `Polynomial.aeval_one` `minpoly.aeval` `Polynomial.aeval_natCast` `MulZeroClass.zero_mul` `add_zero` `Nat.cast_one` `IsPrimitiveRoot.norm_pow_sub_one_eq_prime_pow_of_ne_zero` `le_rfl` `IsPrimitiveRoot.norm_pow_sub_one_of_prime_ne_two` `mul_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `mul_left_inj'` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `eq_zero_of_pow_eq_zero` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `pow_eq_zero_iff` `Nat.cast_pow` `pow_add` `mul_comm` `one_pow` `IsPrimitiveRoot.norm_eq_one` `map_pow` `MonoidHom.instMonoidHomClass` `Algebra.norm_algebraMap` `map_natCast` `RingHom.instRingHomClass` `map_mul` `MonoidHomClass.toMulHomClass`
`discr_prime_pow_ne_two'` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `Nat.instMonoid` `Irreducible` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.cyclotomic`	`Algebra.discr` `PowerBasis.dim` `CommRing.toRing` `IsPrimitiveRoot.powerBasis` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `instIsDomain` `Field.toSemifield` `Fin.fintype` `DFunLike.coe` `Module.Basis` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Module.Basis.instFunLike` `PowerBasis.basis` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toNatCast`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `instIsDomain` `Nat.totient_prime_pow` `Fact.out` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `discr_prime_pow_ne_two`

IsPrimitiveRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`discr_zeta_eq_discr_zeta_sub_one` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Algebra.discr` `PowerBasis.dim` `Rat.instField` `CommRing.toRing` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `powerBasis` `instIsDomain` `Field.toSemifield` `Rat.commRing` `Fin.fintype` `DFunLike.coe` `Module.Basis` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `Module.Basis.instFunLike` `PowerBasis.basis` `subOnePowerBasis`	—	`instIsDomain` `Polynomial.aeval_sub` `Polynomial.aeval_X` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `sub_add_cancel` `Algebra.discr_eq_discr_of_toMatrix_coeff_isIntegral` `IsCyclotomicExtension.finiteDimensional` `Finite.of_fintype` `PowerBasis.toMatrix_isIntegral` `AddCommGroup.intIsScalarTower` `isIntegral` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `minpoly.isIntegrallyClosed_eq_field_fractions'` `Int.instIsDomain` `Rat.isFractionRing` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `IsPrincipalIdealRing.isDedekindDomain` `EuclideanDomain.to_principal_ideal_domain` `IsIntegral.sub` `isIntegral_one`

---

← Back to Index