Basic

📁 Source: Mathlib/NumberTheory/NumberField/Ideal/Basic.lean

Statistics

Metric	Count
Definitions rootsOfUnityMapQuot, torsionMapQuot	2
Theorems rootsOfUnityMapQuot_apply, rootsOfUnityMapQuot_injective, torsionMapQuot_apply, torsionMapQuot_injective, not_coprime_norm_of_mk_eq_one, torsionOrder_dvd_absNorm_sub_one, instFiniteQuotientRingOfIntegersIdealOfNumberFieldOfIsMaximal	7
Total	9

Ideal

Definitions

Name	Category	Theorems
rootsOfUnityMapQuot 📖	CompOp	2 math math: rootsOfUnityMapQuot_injective, rootsOfUnityMapQuot_apply
torsionMapQuot 📖	CompOp	2 math math: torsionMapQuot_apply, torsionMapQuot_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rootsOfUnityMapQuot_apply 📖	mathematical	Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup CommMonoid.toMonoid CommRing.toCommMonoid Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity	Units.val HasQuotient.Quotient Ideal instHasQuotient_1 Quotient.semiring DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Units.instMulOneClass MonoidHom.instFunLike rootsOfUnityMapQuot RingHom Ring.toSemiring CommRing.toRing instHasQuotient Semiring.toNonAssocSemiring Quotient.ring instIsTwoSided_1 RingHom.instFunLike	—	—
rootsOfUnityMapQuot_injective 📖	mathematical	DFunLike.coe MonoidWithZeroHom Ideal NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt	Units CommMonoid.toMonoid CommRing.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity HasQuotient.Quotient instHasQuotient_1 MonoidWithZero.toMonoid Semiring.toMonoidWithZero Quotient.semiring MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Units.instMulOneClass MonoidHom.instFunLike rootsOfUnityMapQuot	—	NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt injective_iff_map_eq_one MonoidHom.instMonoidHomClass isPrimitiveRoot_of_mem_rootsOfUnity IsPrimitiveRoot.map_of_injective MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsPrimitiveRoot.coe_units_iff NumberField.RingOfIntegers.coe_injective IsPrimitiveRoot.not_coprime_norm_of_mk_eq_one instIsTwoSided_1 Units.val_one rootsOfUnityMapQuot_apply Units.ext_iff
torsionMapQuot_apply 📖	mathematical	Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion	Units.val HasQuotient.Quotient Ideal instHasQuotient_1 Quotient.semiring DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Units.instMulOneClass MonoidHom.instFunLike torsionMapQuot RingHom Ring.toSemiring CommRing.toRing instHasQuotient Semiring.toNonAssocSemiring Quotient.ring instIsTwoSided_1 RingHom.instFunLike	—	—
torsionMapQuot_injective 📖	mathematical	DFunLike.coe MonoidWithZeroHom Ideal NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt NumberField.Units.torsionOrder	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion HasQuotient.Quotient instHasQuotient_1 Quotient.semiring MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Units.instMulOneClass MonoidHom.instFunLike torsionMapQuot	—	NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt NumberField.Units.rootsOfUnity_eq_torsion rootsOfUnityMapQuot_injective NumberField.Units.instNeZeroNatTorsionOrder

IsPrimitiveRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_coprime_norm_of_mk_eq_one 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe RingHom NumberField.RingOfIntegers HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing NumberField.RingOfIntegers.instCommRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike toInteger NeZero.of_gt AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Ideal.Quotient.one	MonoidWithZeroHom CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt	—	NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt Ideal.instIsTwoSided_1 NeZero.of_gt Nat.instCanonicallyOrderedAdd Nat.exists_prime_and_dvd Nat.Prime.not_dvd_one prime_dvd_of_dvd_norm_sub_one Ideal.absNorm_dvd_norm_of_mem Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt Ideal.Quotient.eq map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass

NumberField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
torsionOrder_dvd_absNorm_sub_one 📖	—	DFunLike.coe MonoidWithZeroHom Ideal RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring RingOfIntegers.instCommRing NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm RingOfIntegers.instNontrivial RingOfIntegers.instIsDedekindDomain RingOfIntegers.instFreeInt Units.torsionOrder	—	—	RingOfIntegers.instNontrivial RingOfIntegers.instIsDedekindDomain RingOfIntegers.instFreeInt Ring.DimensionLEOne.maximalOfPrime IsDedekindDomainDvr.ring_dimensionLEOne RingOfIntegers.instIsDomain IsDedekindDomain.isDedekindDomainDvr Iff.not Ideal.absNorm_eq_one_iff Ideal.IsPrime.ne_top Subgroup.card_dvd_of_injective Ideal.torsionMapQuot_injective Nat.card_units Nat.card_eq_fintype_card

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFiniteQuotientRingOfIntegersIdealOfNumberFieldOfIsMaximal 📖	mathematical	—	Finite HasQuotient.Quotient NumberField.RingOfIntegers Ideal CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Ideal.instHasQuotient_1	—	Ideal.finiteQuotientOfFreeOfNeBot NumberField.RingOfIntegers.instIsDomain NumberField.RingOfIntegers.instFreeInt Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt LT.lt.ne' Ideal.bot_lt_of_maximal NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.not_isField

---

← Back to Index