IsPrincipal

📁 Source: Mathlib/RingTheory/Ideal/IsPrincipal.lean

Statistics

Metric	Count
Definitions associatesEquivIsPrincipal, associatesMulEquivIsPrincipal, associatesNonZeroDivisorsEquivIsPrincipal, associatesNonZeroDivisorsMulEquivIsPrincipal, isPrincipalNonZeroDivisorsSubmonoid, isPrincipalSubmonoid, isoBaseOfIsPrincipal, IsPrincipal, IsPrincipal	9
Theorems associatesEquivIsPrincipal_apply, associatesEquivIsPrincipal_map_one, associatesEquivIsPrincipal_map_zero, associatesEquivIsPrincipal_mul, associatesEquivIsPrincipal_symm_apply, associatesNonZeroDivisorsEquivIsPrincipal_apply, associatesNonZeroDivisorsEquivIsPrincipal_coe, associatesNonZeroDivisorsEquivIsPrincipal_map_one, associatesNonZeroDivisorsEquivIsPrincipal_mul, isoBaseOfIsPrincipal_apply, mem_isPrincipalSubmonoid_iff, span_singleton_mem_isPrincipalSubmonoid, subtype_isoBaseOfIsPrincipal_eq_mul	13
Total	22

Ideal

Definitions

Name	Category	Theorems
associatesEquivIsPrincipal 📖	CompOp	6 math math: associatesEquivIsPrincipal_symm_apply, associatesEquivIsPrincipal_apply, associatesEquivIsPrincipal_mul, associatesEquivIsPrincipal_map_zero, associatesNonZeroDivisorsEquivIsPrincipal_coe, associatesEquivIsPrincipal_map_one
associatesMulEquivIsPrincipal 📖	CompOp	—
associatesNonZeroDivisorsEquivIsPrincipal 📖	CompOp	4 math math: associatesNonZeroDivisorsEquivIsPrincipal_apply, associatesNonZeroDivisorsEquivIsPrincipal_mul, associatesNonZeroDivisorsEquivIsPrincipal_map_one, associatesNonZeroDivisorsEquivIsPrincipal_coe
associatesNonZeroDivisorsMulEquivIsPrincipal 📖	CompOp	—
isPrincipalNonZeroDivisorsSubmonoid 📖	CompOp	—
isPrincipalSubmonoid 📖	CompOp	2 math math: span_singleton_mem_isPrincipalSubmonoid, mem_isPrincipalSubmonoid_iff
isoBaseOfIsPrincipal 📖	CompOp	2 math math: subtype_isoBaseOfIsPrincipal_eq_mul, isoBaseOfIsPrincipal_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associatesEquivIsPrincipal_apply 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe Equiv Associates MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike Equiv.instEquivLike associatesEquivIsPrincipal span Set Set.instSingletonSet	—	—
associatesEquivIsPrincipal_map_one 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe Equiv Associates MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike Equiv.instEquivLike associatesEquivIsPrincipal Associates.instOne Submodule.one	—	Associates.one_eq_mk_one associatesEquivIsPrincipal_apply span_singleton_one one_eq_top
associatesEquivIsPrincipal_map_zero 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe Equiv Associates MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike Equiv.instEquivLike associatesEquivIsPrincipal Associates.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule.pointwiseZero	—	Associates.mk_zero associatesEquivIsPrincipal_apply Submodule.zero_eq_bot span_singleton_eq_bot
associatesEquivIsPrincipal_mul 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe Equiv Associates MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike Equiv.instEquivLike associatesEquivIsPrincipal Associates.instMul CommRing.toCommMonoid Submodule.mul IsScalarTower.right Algebra.id	—	IsScalarTower.right Associates.quot_out span_singleton_mul_span_singleton instIsTwoSided_1
associatesEquivIsPrincipal_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Associates MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike Equiv.instEquivLike Equiv.symm associatesEquivIsPrincipal Submodule.IsPrincipal.generator	—	—
associatesNonZeroDivisorsEquivIsPrincipal_apply 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe Equiv Associates Submonoid.toMonoid MonoidWithZero.toMonoid EquivLike.toFunLike Equiv.instEquivLike associatesNonZeroDivisorsEquivIsPrincipal span Set Set.instSingletonSet	—	—
associatesNonZeroDivisorsEquivIsPrincipal_coe 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe Equiv Associates Submonoid.toMonoid MonoidWithZero.toMonoid EquivLike.toFunLike Equiv.instEquivLike associatesNonZeroDivisorsEquivIsPrincipal associatesEquivIsPrincipal CommMonoidWithZero.toMonoidWithZero CommSemiring.toCommMonoidWithZero Associates.instCommMonoidWithZero MulEquiv Associates.instMul Submonoid.toCommMonoid CommMonoidWithZero.toCommMonoid Submonoid.mul MulEquiv.instEquivLike MulEquiv.symm associatesNonZeroDivisorsEquiv	—	—
associatesNonZeroDivisorsEquivIsPrincipal_map_one 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe Equiv Associates Submonoid.toMonoid MonoidWithZero.toMonoid EquivLike.toFunLike Equiv.instEquivLike associatesNonZeroDivisorsEquivIsPrincipal Associates.instOne Submodule.one	—	associatesNonZeroDivisorsEquivIsPrincipal_coe map_one MonoidHomClass.toOneHomClass MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass OneMemClass.coe_one associatesEquivIsPrincipal_map_one
associatesNonZeroDivisorsEquivIsPrincipal_mul 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe Equiv Associates Submonoid.toMonoid MonoidWithZero.toMonoid EquivLike.toFunLike Equiv.instEquivLike associatesNonZeroDivisorsEquivIsPrincipal Associates.instMul Submonoid.toCommMonoid CommRing.toCommMonoid Submodule.mul IsScalarTower.right	—	IsScalarTower.right map_mul MonoidHomClass.toMulHomClass MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass associatesEquivIsPrincipal_mul
isoBaseOfIsPrincipal_apply 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule.addCommMonoid Submodule.module EquivLike.toFunLike LinearEquiv.instEquivLike isoBaseOfIsPrincipal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Submodule.IsPrincipal.generator	—	RingHomInvPair.ids
mem_isPrincipalSubmonoid_iff 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike isPrincipalSubmonoid Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	—
span_singleton_mem_isPrincipalSubmonoid 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike isPrincipalSubmonoid span Set Set.instSingletonSet	—	mem_isPrincipalSubmonoid_iff
subtype_isoBaseOfIsPrincipal_eq_mul 📖	mathematical	—	LinearMap.comp Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SetLike.instMembership Submodule.setLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule.addCommMonoid Submodule.module RingHom.id RingHomCompTriple.ids Submodule.subtype LinearEquiv.toLinearMap RingHomInvPair.ids Ideal isoBaseOfIsPrincipal DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike LinearMap.mul Algebra.to_smulCommClass Algebra.id IsScalarTower.right Submodule.IsPrincipal.generator	—	LinearMap.ext_ring RingHomCompTriple.ids RingHomInvPair.ids smulCommClass_self Algebra.to_smulCommClass IsScalarTower.right one_mul mul_one

Module

Definitions

Name	Category	Theorems
IsPrincipal 📖	MathDef	4 math math: IsPrincipal.of_surjective, isPrincipal_submodule_iff, isPrincipal_def, LinearEquiv.isPrincipal_iff

Submodule

Definitions

Name	Category	Theorems
IsPrincipal 📖	CompData	62 math math: IsPrincipal.of_comap, FractionalIdeal.isPrincipal_of_isPrincipal_num, NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, IsPrincipal.map_ringHom, Valuation.Integers.isPrincipal_iff_exists_isGreatest, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_apply, instIsPrincipalSpanSingletonSet, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le, maximalIdeal_isPrincipal_of_isDedekindDomain, ClassGroup.mk0_eq_one_iff, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, Ideal.IsPrincipal.of_finite_maximals_of_isUnit, NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv_apply_fst, nonPrincipals_eq_empty_iff, top_isPrincipal, Valuation.ideal_isPrincipal, isPrincipalIdealRing_iff, FractionalIdeal.isPrincipal_iff, bot_isPrincipal, Ideal.setOf_isPrincipal_wellFoundedOn_gt, tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain, IsBezout.iff_span_pair_isPrincipal, FractionalIdeal.isPrincipal_of_unit_of_comap_mul_span_singleton_eq_top, isPrincipal_iff, instIsPrincipalSpanSingletonSet, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_mul, FractionalIdeal.isPrincipal_inv, ClassGroup.mk_eq_one_iff, IsLocalRing.finrank_cotangentSpace_le_one_iff, IsPrincipal.map, Ideal.associatesEquivIsPrincipal_symm_apply, Module.isPrincipal_submodule_iff, Ideal.exists_maximal_not_isPrincipal, IsSimpleModule.instIsPrincipal, Module.exists_isPrincipal_quotient_of_finite, Ideal.associatesEquivIsPrincipal_apply, IsBezout.isPrincipal_of_FG, nonPrincipals_def, instIsPrincipalMapRingHom, Module.rank_le_one_iff_top_isPrincipal, FractionalIdeal.isPrincipal.of_finite_maximals_of_inv, Valuation.Integers.isPrincipal_iff_exists_eq_setOf_valuation_le, IsDiscreteValuationRing.TFAE, finrank_le_one_iff_isPrincipal, ClassGroup.isPrincipal_coeSubmodule_of_isUnit, Ideal.associatesEquivIsPrincipal_mul, Ideal.mem_isPrincipalSubmonoid_iff, rank_le_one_iff_isPrincipal, Ideal.associatesEquivIsPrincipal_map_zero, FractionalIdeal.isPrincipal, IsFractionRing.coeSubmodule_isPrincipal, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_map_one, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_coe, Ideal.IsPrincipal.of_comap, Module.isPrincipal_def, IsLocalization.coeSubmodule_isPrincipal, IsPrincipalIdealRing.principal, IsBezout.span_pair_isPrincipal, Ideal.associatesEquivIsPrincipal_map_one, ClassGroup.isPrincipal_of_isUnit_coeIdeal, Module.finrank_le_one_iff_top_isPrincipal, Ideal.isOka_isPrincipal

---

← Back to Index