Basic

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

Statistics

Metric	Count
Definitions rootsOfUnityMapQuot, torsionMapQuot	2
Theorems rootsOfUnityMapQuot_apply, rootsOfUnityMapQuot_injective, torsionMapQuot_apply, torsionMapQuot_injective, idealQuotient_mk, not_coprime_norm_of_mk_eq_one, torsionOrder_dvd_absNorm_sub_one, instFiniteQuotientRingOfIntegersIdealOfNumberFieldOfIsMaximal	8
Total	10

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.instCommRingRingOfIntegers Subgroup CommMonoid.toMonoid CommRing.toCommMonoid Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity	Units.val HasQuotient.Quotient NumberField.RingOfIntegers Ideal CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers instHasQuotient_1 MonoidWithZero.toMonoid Semiring.toMonoidWithZero Quotient.semiring DFunLike.coe MonoidHom Units CommMonoid.toMonoid CommRing.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity 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.instCommRingRingOfIntegers NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm NumberField.instNontrivialRingOfIntegers NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt	Units NumberField.RingOfIntegers CommMonoid.toMonoid CommRing.toCommMonoid NumberField.instCommRingRingOfIntegers Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring instHasQuotient_1 MonoidWithZero.toMonoid Semiring.toMonoidWithZero Quotient.semiring DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Units.instMulOneClass MonoidHom.instFunLike rootsOfUnityMapQuot	—	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.instCommRingRingOfIntegers Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion	Units.val HasQuotient.Quotient NumberField.RingOfIntegers Ideal CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers instHasQuotient_1 MonoidWithZero.toMonoid Semiring.toMonoidWithZero Quotient.semiring DFunLike.coe MonoidHom Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion 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.instCommRingRingOfIntegers NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike absNorm NumberField.instNontrivialRingOfIntegers NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt NumberField.Units.torsionOrder	Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion 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	—	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
idealQuotient_mk 📖	mathematical	IsPrimitiveRoot NumberField.RingOfIntegers CommRing.toCommMonoid NumberField.instCommRingRingOfIntegers DFunLike.coe MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm NumberField.instNontrivialRingOfIntegers NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt	IsPrimitiveRoot HasQuotient.Quotient NumberField.RingOfIntegers Ideal Ring.toSemiring CommRing.toRing NumberField.instCommRingRingOfIntegers Ideal.instHasQuotient CommRing.toCommMonoid Ideal.Quotient.commRing DFunLike.coe RingHom Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike	—	NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt coe_submonoidClass_iff coe_units_iff map_of_injective MonoidHom.instMonoidHomClass Ideal.rootsOfUnityMapQuot_injective
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.instCommRingRingOfIntegers 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	DFunLike.coe MonoidWithZeroHom Ideal NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm NumberField.instNontrivialRingOfIntegers NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt	—	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 AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg NumberField.RingOfIntegers.instFG 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 📖	mathematical	DFunLike.coe MonoidWithZeroHom Ideal RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring instCommRingRingOfIntegers NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm instNontrivialRingOfIntegers RingOfIntegers.instIsDedekindDomain RingOfIntegers.instFreeInt Units.torsionOrder	Units.torsionOrder DFunLike.coe MonoidWithZeroHom Ideal RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring instCommRingRingOfIntegers NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm instNontrivialRingOfIntegers RingOfIntegers.instIsDedekindDomain RingOfIntegers.instFreeInt	—	RingOfIntegers.instIsDedekindDomain RingOfIntegers.instFreeInt Ring.DimensionLEOne.maximalOfPrime IsDedekindDomainDvr.ring_dimensionLEOne 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.instCommRingRingOfIntegers Ideal.instHasQuotient_1	—	Ideal.finiteQuotientOfFreeOfNeBot NumberField.RingOfIntegers.instFreeInt AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg NumberField.RingOfIntegers.instFG LT.lt.ne' Ideal.bot_lt_of_maximal NumberField.RingOfIntegers.not_isField

---

← Back to Index