ClassGroup

📁 Source: Mathlib/RingTheory/ClassGroup.lean

Statistics

Metric	Count
Definitions equiv, integralRep, mk, mk0, mulEquivUnitsSubmoduleQuotRange, mk0, instCommGroupClassGroup, instFintypeClassGroupOfIsPrincipalIdealRing, instInhabitedClassGroup, toPrincipalIdeal	10
Theorems Quot_mk_eq_mk, equiv_mk, equiv_mk0, induction, integralRep_mem_nonZeroDivisors, isPrincipal_coeSubmodule_of_isUnit, isPrincipal_of_isUnit_coeIdeal, mk0_eq_mk0_iff, mk0_eq_mk0_iff_exists_fraction_ring, mk0_eq_mk0_inv_iff, mk0_eq_one_iff, mk0_integralRep, mk0_surjective, mk_canonicalEquiv, mk_def, mk_eq_mk, mk_eq_mk_of_coe_ideal, mk_eq_one_iff, mk_eq_one_of_coe_ideal, mk_mk0, canonicalEquiv_mk0, coe_mk0, isUnit_num, map_canonicalEquiv_mk0, normal, card_classGroup_eq_one, card_classGroup_eq_one_iff, coe_toPrincipalIdeal, mem_principal_ideals_iff, toPrincipalIdeal_def, toPrincipalIdeal_eq_iff	31
Total	41

ClassGroup

Definitions

Name	Category	Theorems
equiv 📖	CompOp	2 math math: equiv_mk0, equiv_mk
integralRep 📖	CompOp	1 math math: mk0_integralRep
mk 📖	CompOp	—
mk0 📖	CompOp	—
mulEquivUnitsSubmoduleQuotRange 📖	CompOp	2 math math: equivPic_symm_apply, equivPic_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Quot_mk_eq_mk 📖	mathematical	—	Units FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring FractionRing OreLocalization.instCommRing OreLocalization.oreSetComm CommRing.toCommMonoid OreLocalization.instAlgebra Algebra.id MonoidWithZero.toMonoid FractionalIdeal.commSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain FractionRing.field QuotientGroup.leftRel Units.instGroup MonoidHom.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toPrincipalIdeal DFunLike.coe MonoidHom ClassGroup MulOneClass.toMulOne Units.instMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup MonoidHom.instFunLike Localization.isLocalization	—	Localization.isLocalization PrincipalIdeals.normal MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass mk_def FractionalIdeal.canonicalEquiv_self RingEquiv.coe_monoidHom_refl Units.map_id MonoidHom.id_apply QuotientGroup.mk'_apply
equiv_mk 📖	mathematical	—	DFunLike.coe MulEquiv ClassGroup HasQuotient.Quotient Units FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidWithZero.toMonoid FractionalIdeal.commSemiring Subgroup Units.instGroup QuotientGroup.instHasQuotientSubgroup MonoidHom.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toPrincipalIdeal MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup QuotientGroup.Quotient.group PrincipalIdeals.normal EquivLike.toFunLike MulEquiv.instEquivLike equiv MonoidHom Units.instMulOneClass MonoidHom.instFunLike QuotientGroup.mk' Units.instMul Units.mapEquiv MulEquivClass.toMulEquiv RingEquiv FractionalIdeal.instMul FractionalIdeal.instAdd RingEquiv.instEquivLike RingEquivClass.toMulEquivClass RingEquiv.instRingEquivClass FractionalIdeal.canonicalEquiv	—	PrincipalIdeals.normal RingEquivClass.toMulEquivClass RingEquiv.instRingEquivClass equiv.eq_1 Localization.isLocalization MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass mk_def Units.coe_mapEquiv Units.coe_map FractionalIdeal.canonicalEquiv_canonicalEquiv
equiv_mk0 📖	mathematical	—	DFunLike.coe MulEquiv ClassGroup HasQuotient.Quotient Units FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidWithZero.toMonoid FractionalIdeal.commSemiring Subgroup Units.instGroup QuotientGroup.instHasQuotientSubgroup MonoidHom.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toPrincipalIdeal MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup QuotientGroup.Quotient.group PrincipalIdeals.normal EquivLike.toFunLike MulEquiv.instEquivLike equiv MonoidHom Ideal Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike Submonoid.toMulOneClass MonoidHom.instFunLike QuotientGroup.mk' FractionalIdeal.semifield Units.instMulOneClass	—	PrincipalIdeals.normal MonoidHom.comp_apply RingEquivClass.toMulEquivClass RingEquiv.instRingEquivClass FractionalIdeal.canonicalEquiv_coeIdeal
induction 📖	—	DFunLike.coe MonoidHom Units FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidWithZero.toMonoid FractionalIdeal.commSemiring ClassGroup MulOneClass.toMulOne Units.instMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup MonoidHom.instFunLike	—	—	QuotientGroup.induction_on Localization.isLocalization RingEquivClass.toMulEquivClass RingEquiv.instRingEquivClass FractionalIdeal.canonicalEquiv_canonicalEquiv FractionalIdeal.canonicalEquiv_self
integralRep_mem_nonZeroDivisors 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors FractionalIdeal.num FractionRing OreLocalization.instCommRing OreLocalization.oreSetComm CommRing.toCommMonoid OreLocalization.instAlgebra	—	mem_nonZeroDivisors_iff_ne_zero Ideal.instNoZeroDivisors IsDomain.to_noZeroDivisors Ideal.instNontrivial IsDomain.toNontrivial FractionalIdeal.num_eq_zero_iff Localization.isLocalization
isPrincipal_coeSubmodule_of_isUnit 📖	mathematical	IsUnit FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidWithZero.toMonoid FractionalIdeal.commSemiring	Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule FractionalIdeal.coeToSubmodule	—	mk_eq_one_iff
isPrincipal_of_isUnit_coeIdeal 📖	mathematical	IsUnit FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidWithZero.toMonoid FractionalIdeal.commSemiring FractionalIdeal.coeIdeal	Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	isPrincipal_coeSubmodule_of_isUnit IsFractionRing.coeSubmodule_isPrincipal
mk0_eq_mk0_iff 📖	mathematical	—	DFunLike.coe MonoidHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors ClassGroup MulOneClass.toMulOne Submonoid.toMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup MonoidHom.instFunLike Submodule.mul Semiring.toModule IsScalarTower.right Ideal.span Set Set.instSingletonSet	—	Localization.isLocalization IsScalarTower.right IsLocalization.exists_mk'_eq IsFractionRing.mk'_eq_div map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsDomain.toNontrivial IsDomain.to_noZeroDivisors zero_div mem_nonZeroDivisors_iff_ne_zero FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal Mathlib.Tactic.Contrapose.contrapose₄ IsFractionRing.injective RingHom.map_zero MulZeroClass.zero_mul IsLocalization.mk'_eq_iff_eq_mul
mk0_eq_mk0_iff_exists_fraction_ring 📖	mathematical	—	DFunLike.coe MonoidHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors ClassGroup MulOneClass.toMulOne Submonoid.toMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup MonoidHom.instFunLike FractionalIdeal EuclideanDomain.toCommRing Field.toEuclideanDomain FractionalIdeal.instMul FractionalIdeal.spanSingleton FractionalIdeal.coeIdeal	—	PrincipalIdeals.normal MulEquiv.injective equiv_mk0 FractionalIdeal.spanSingleton_zero Units.ne_zero FractionalIdeal.instNontrivialNonZeroDivisors mul_comm FractionalIdeal.spanSingleton_ne_zero_iff
mk0_eq_mk0_inv_iff 📖	mathematical	—	DFunLike.coe MonoidHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors ClassGroup MulOneClass.toMulOne Submonoid.toMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup MonoidHom.instFunLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Submodule.mul Semiring.toModule IsScalarTower.right Ideal.span Set Set.instSingletonSet	—	IsScalarTower.right eq_inv_iff_mul_eq_one map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass Submodule.isPrincipal_iff Submonoid.coe_mul nonZeroDivisors.coe_ne_zero Ideal.instNontrivial IsDomain.toNontrivial Subtype.prop Submodule.span_zero_singleton
mk0_eq_one_iff 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	DFunLike.coe MonoidHom ClassGroup MulOneClass.toMulOne Submonoid.toMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup MonoidHom.instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	mk_eq_one_iff IsFractionRing.coeSubmodule_isPrincipal Localization.isLocalization
mk0_integralRep 📖	mathematical	—	DFunLike.coe MonoidHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors ClassGroup MulOneClass.toMulOne Submonoid.toMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup MonoidHom.instFunLike integralRep Units.val FractionalIdeal FractionRing OreLocalization.instCommRing OreLocalization.oreSetComm CommRing.toCommMonoid OreLocalization.instAlgebra MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield FractionRing.field Localization.isLocalization integralRep_mem_nonZeroDivisors Units.ne_zero FractionalIdeal.instNontrivialNonZeroDivisors Units EuclideanDomain.toCommRing Field.toEuclideanDomain FractionalIdeal.commSemiring Units.instMulOneClass	—	Localization.isLocalization integralRep_mem_nonZeroDivisors Units.ne_zero FractionalIdeal.instNontrivialNonZeroDivisors mk_mk0 IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors IsDomain.toNontrivial SetLike.coe_mem IsDomain.to_noZeroDivisors Units.ext mul_comm Units.val_mul coe_toPrincipalIdeal Units.val_mk0 FractionalIdeal.den_mul_self_eq_num'
mk0_surjective 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors ClassGroup DFunLike.coe MonoidHom MulOneClass.toMulOne Submonoid.toMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup MonoidHom.instFunLike	—	integralRep_mem_nonZeroDivisors Units.ne_zero Localization.isLocalization FractionalIdeal.instNontrivialNonZeroDivisors
mk_canonicalEquiv 📖	mathematical	—	DFunLike.coe MonoidHom Units FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidWithZero.toMonoid FractionalIdeal.commSemiring ClassGroup MulOneClass.toMulOne Units.instMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup MonoidHom.instFunLike Units.map MonoidHomClass.toMonoidHom RingEquiv FractionalIdeal.instMul FractionalIdeal.instAdd EquivLike.toFunLike RingEquiv.instEquivLike MonoidWithZeroHomClass.toMonoidHomClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass FractionalIdeal.canonicalEquiv	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass Localization.isLocalization PrincipalIdeals.normal mk_def MonoidHom.comp_apply Units.map_comp RingEquiv.coe_monoidHom_trans FractionalIdeal.canonicalEquiv_trans_canonicalEquiv
mk_def 📖	mathematical	—	DFunLike.coe MonoidHom Units FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidWithZero.toMonoid FractionalIdeal.commSemiring ClassGroup MulOneClass.toMulOne Units.instMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup MonoidHom.instFunLike FractionRing FractionRing.field OreLocalization.instAlgebra OreLocalization.oreSetComm CommRing.toCommMonoid Algebra.id HasQuotient.Quotient Subgroup Units.instGroup QuotientGroup.instHasQuotientSubgroup MonoidHom.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toPrincipalIdeal Localization.isLocalization QuotientGroup.Quotient.group PrincipalIdeals.normal QuotientGroup.mk' Units.map MonoidHomClass.toMonoidHom RingEquiv OreLocalization.instCommRing FractionalIdeal.instMul FractionalIdeal.instAdd EquivLike.toFunLike RingEquiv.instEquivLike MonoidWithZeroHomClass.toMonoidHomClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass FractionalIdeal.canonicalEquiv	—	—
mk_eq_mk 📖	mathematical	—	DFunLike.coe MonoidHom Units FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring FractionRing EuclideanDomain.toCommRing Field.toEuclideanDomain FractionRing.field OreLocalization.instAlgebra OreLocalization.oreSetComm CommRing.toCommMonoid Algebra.id MonoidWithZero.toMonoid FractionalIdeal.commSemiring ClassGroup MulOneClass.toMulOne Units.instMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup MonoidHom.instFunLike Localization.isLocalization OreLocalization.instCommRing Units.instMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toPrincipalIdeal	—	Localization.isLocalization PrincipalIdeals.normal MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass mk_def QuotientGroup.mk'_eq_mk' MonoidHomClass.toMonoidHom.congr_simp FractionalIdeal.canonicalEquiv_self Units.map_id
mk_eq_mk_of_coe_ideal 📖	mathematical	Units.val FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring FractionRing OreLocalization.instCommRing OreLocalization.oreSetComm CommRing.toCommMonoid OreLocalization.instAlgebra Algebra.id MonoidWithZero.toMonoid FractionalIdeal.commSemiring FractionalIdeal.coeIdeal	DFunLike.coe MonoidHom Units EuclideanDomain.toCommRing Field.toEuclideanDomain FractionRing.field ClassGroup MulOneClass.toMulOne Units.instMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup MonoidHom.instFunLike Localization.isLocalization Ideal Submodule.mul Semiring.toModule IsScalarTower.right Ideal.span Set Set.instSingletonSet	—	Localization.isLocalization IsScalarTower.right IsLocalization.sec_fst_ne_zero Units.ne_zero FractionRing.instNontrivial IsDomain.toNontrivial IsLocalization.sec_snd_ne_zero le_rfl FractionalIdeal.spanSingleton_mul_coeIdeal_eq_coeIdeal mul_comm coe_toPrincipalIdeal Units.val_mul mem_nonZeroDivisors_of_ne_zero IsDomain.to_noZeroDivisors FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal
mk_eq_one_iff 📖	mathematical	—	DFunLike.coe MonoidHom Units FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidWithZero.toMonoid FractionalIdeal.commSemiring ClassGroup MulOneClass.toMulOne Units.instMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup MonoidHom.instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule FractionalIdeal.coeToSubmodule Units.val	—	PrincipalIdeals.normal MulEquiv.injective RingEquivClass.toMulEquivClass RingEquiv.instRingEquivClass MulEquivClass.toMulEquiv.congr_simp FractionalIdeal.canonicalEquiv_self map_one MonoidHomClass.toOneHomClass MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass Subgroup.normal_of_comm coe_toPrincipalIdeal FractionalIdeal.coe_spanSingleton Submodule.IsPrincipal.principal Subtype.coe_injective Units.ne_zero FractionalIdeal.instNontrivialNonZeroDivisors FractionalIdeal.spanSingleton.congr_simp FractionalIdeal.spanSingleton_zero
mk_eq_one_of_coe_ideal 📖	mathematical	Units.val FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring FractionRing OreLocalization.instCommRing OreLocalization.oreSetComm CommRing.toCommMonoid OreLocalization.instAlgebra Algebra.id MonoidWithZero.toMonoid FractionalIdeal.commSemiring FractionalIdeal.coeIdeal	DFunLike.coe MonoidHom Units EuclideanDomain.toCommRing Field.toEuclideanDomain FractionRing.field ClassGroup MulOneClass.toMulOne Units.instMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup MonoidHom.instFunLike Localization.isLocalization InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Ideal.span Set Set.instSingletonSet	—	Localization.isLocalization map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass IsScalarTower.right mk_eq_mk_of_coe_ideal Ideal.mem_span_singleton_mul Ideal.span_singleton_le_iff_mem Eq.ge IsScalarTower.left Ideal.mul_top Ideal.instIsTwoSided_1 Ideal.span_singleton_mul_span_singleton one_ne_zero NeZero.one IsDomain.toNontrivial Ideal.span_singleton_one Ideal.top_mul
mk_mk0 📖	mathematical	—	DFunLike.coe MonoidHom Units FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidWithZero.toMonoid FractionalIdeal.commSemiring ClassGroup MulOneClass.toMulOne Units.instMulOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup MonoidHom.instFunLike Ideal Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring FractionalIdeal.semifield Submonoid.toMulOneClass	—	MonoidHom.comp_apply Localization.isLocalization MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass mk_canonicalEquiv FractionalIdeal.map_canonicalEquiv_mk0

FractionalIdeal

Definitions

Name	Category	Theorems
mk0 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canonicalEquiv_mk0 📖	mathematical	—	DFunLike.coe RingEquiv FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain instMul instAdd EquivLike.toFunLike RingEquiv.instEquivLike canonicalEquiv Units.val MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring semifield MonoidHom Ideal Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike Units MulOneClass.toMulOne Submonoid.toMulOneClass Units.instMulOneClass MonoidHom.instFunLike	—	canonicalEquiv_coeIdeal
coe_mk0 📖	mathematical	—	Units.val FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring semifield DFunLike.coe MonoidHom Ideal Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike Units MulOneClass.toMulOne Submonoid.toMulOneClass Units.instMulOneClass MonoidHom.instFunLike coeIdeal	—	—
isUnit_num 📖	mathematical	—	IsUnit FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring FractionRing OreLocalization.instCommRing OreLocalization.oreSetComm CommRing.toCommMonoid OreLocalization.instAlgebra Algebra.id MonoidWithZero.toMonoid commSemiring coeIdeal num	—	IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors Localization.isLocalization IsDomain.toNontrivial Subtype.prop IsDomain.to_noZeroDivisors coe_toPrincipalIdeal den_mul_self_eq_num' Units.isUnit_units_mul
map_canonicalEquiv_mk0 📖	mathematical	—	DFunLike.coe MonoidHom Units FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidWithZero.toMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring semifield MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Units.map MonoidHomClass.toMonoidHom RingEquiv instMul instAdd Monoid.toMulOneClass EquivLike.toFunLike RingEquiv.instEquivLike MonoidWithZeroHomClass.toMonoidHomClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass canonicalEquiv Ideal Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike Submonoid.toMulOneClass	—	Units.ext MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass canonicalEquiv_mk0

PrincipalIdeals

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
normal 📖	mathematical	—	Subgroup.Normal Units FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidWithZero.toMonoid FractionalIdeal.commSemiring Units.instGroup MonoidHom.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toPrincipalIdeal	—	Subgroup.normal_of_comm

(root)

Definitions

Name	Category	Theorems
instCommGroupClassGroup 📖	CompOp	28 math math: ClassGroup.mk0_integralRep, ClassGroup.mk0_eq_mk0_iff, ClassGroup.mk_eq_mk_of_coe_ideal, ClassGroup.Quot_mk_eq_mk, WeierstrassCurve.Affine.Point.toClass_zero, ClassGroup.mk0_eq_one_iff, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul, ClassGroup.mk_mk0, ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring, ClassGroup.mk_eq_one_iff, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal', ClassGroup.mk_eq_mk, ClassGroup.equivPic_symm_apply, WeierstrassCurve.Affine.Point.toClass_some, NumberField.exists_ideal_in_class_of_norm_le, WeierstrassCurve.Affine.Point.toClass_injective, ClassGroup.exists_mk0_eq_mk0, ClassGroup.mk0_surjective, ClassGroup.mk_eq_one_of_coe_ideal, WeierstrassCurve.Affine.Point.toClass_eq_zero, ClassGroup.equiv_mk0, NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop, ClassGroup.mk0_eq_mk0_inv_iff, ClassGroup.mk_canonicalEquiv, ClassGroup.equivPic_apply, ClassGroup.mk_def, WeierstrassCurve.Affine.Point.toClass_apply, ClassGroup.equiv_mk
instFintypeClassGroupOfIsPrincipalIdealRing 📖	CompOp	1 math math: card_classGroup_eq_one
instInhabitedClassGroup 📖	CompOp	—
toPrincipalIdeal 📖	CompOp	10 math math: ClassGroup.Quot_mk_eq_mk, mem_principal_ideals_iff, coe_toPrincipalIdeal, PrincipalIdeals.normal, toPrincipalIdeal_eq_iff, ClassGroup.mk_eq_mk, toPrincipalIdeal_def, ClassGroup.equiv_mk0, ClassGroup.mk_def, ClassGroup.equiv_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_classGroup_eq_one 📖	mathematical	—	Fintype.card ClassGroup instFintypeClassGroupOfIsPrincipalIdealRing	—	Fintype.card_eq_one_iff ClassGroup.induction Localization.isLocalization ClassGroup.mk_eq_one_iff FractionalIdeal.isPrincipal
card_classGroup_eq_one_iff 📖	mathematical	—	Fintype.card ClassGroup IsPrincipalIdealRing CommSemiring.toSemiring CommRing.toCommSemiring	—	Fintype.card_eq_one_iff bot_isPrincipal mem_nonZeroDivisors_iff_ne_zero Ideal.instNoZeroDivisors IsDomain.to_noZeroDivisors Ideal.instNontrivial IsDomain.toNontrivial Fintype.card_congr' card_classGroup_eq_one
coe_toPrincipalIdeal 📖	mathematical	—	Units.val FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidWithZero.toMonoid FractionalIdeal.commSemiring DFunLike.coe MonoidHom Units DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike toPrincipalIdeal FractionalIdeal.spanSingleton	—	toPrincipalIdeal_def
mem_principal_ideals_iff 📖	mathematical	—	Units FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidWithZero.toMonoid FractionalIdeal.commSemiring Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidHom.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toPrincipalIdeal FractionalIdeal.spanSingleton Units.val	—	FractionalIdeal.spanSingleton_zero Units.ne_zero FractionalIdeal.instNontrivialNonZeroDivisors
toPrincipalIdeal_def 📖	mathematical	—	toPrincipalIdeal Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield FractionalIdeal nonZeroDivisors CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain FractionalIdeal.commSemiring MulOneClass.toMulOne Units.instMulOneClass MulOne.toOne FractionalIdeal.spanSingleton Units.val InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	—
toPrincipalIdeal_eq_iff 📖	mathematical	—	DFunLike.coe MonoidHom Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield FractionalIdeal nonZeroDivisors CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain FractionalIdeal.commSemiring MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike toPrincipalIdeal FractionalIdeal.spanSingleton Units.val	—	toPrincipalIdeal_def Units.ext_iff

---

← Back to Index