Documentation Verification Report

IsPrincipal

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

Statistics

Metric	Count
Definitions `associatesEquivIsPrincipal`, `associatesMulEquivIsPrincipal`, `associatesNonZeroDivisorsEquivIsPrincipal`, `associatesNonZeroDivisorsMulEquivIsPrincipal`, `isPrincipalNonZeroDivisorsSubmonoid`, `isPrincipalSubmonoid`, `isoBaseOfIsPrincipal`, `IsPrincipal`, `IsPrincipal`, `IsPrincipal`	10
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	23

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`

Ordinal

Definitions

Name	Category	Theorems
`IsPrincipal` 📖	MathDef	75 math math: `isPrincipal_add_iff_add_self_lt`, `principal_add_omega`, `isPrincipal_swap_iff`, `isPrincipal_iff_of_monotone`, `isPrincipal_add_iff_zero_or_omega0_opow`, `principal_mul_of_le_two`, `isPrincipal_add_ord`, `principal_add_of_le_one`, `principal_opow_ord`, `principal_add_ord`, `isPrincipal_add_one`, `isPrincipal_mul_omega0_opow_opow`, `principal_mul_omega0`, `isPrincipal_zero`, `IsInitial.principal_mul`, `Principal.sSup`, `principal_opow_omega0`, `not_bddAbove_principal`, `isPrincipal_mul_omega0`, `principal_add_iff_add_left_eq_self`, `principal_mul_ord`, `isPrincipal_add_of_isPrincipal_mul`, `not_isPrincipal_iff`, `isPrincipal_one_iff`, `not_bddAbove_setOf_isPrincipal`, `isPrincipal_opow_omega0`, `IsInitial.principal_opow`, `Principal.iSup`, `isPrincipal_add_iff_add_lt_ne_self`, `isPrincipal_add_opow_of_isPrincipal_add`, `not_principal_iff_of_monotone`, `principal_mul_omega`, `principal_add_iff_zero_or_omega0_opow`, `principal_add_iff_add_lt_ne_self`, `principal_add_mul_of_principal_add`, `principal_add_of_principal_mul`, `isPrincipal_opow_ord`, `isPrincipal_add_omega0`, `IsPrincipal.iSup`, `not_principal_iff`, `IsInitial.isPrincipal_mul`, `isPrincipal_add_omega`, `IsInitial.isPrincipal_add`, `principal_one_iff`, `isPrincipal_mul_of_le_two`, `isPrincipal_add_iff_add_left_eq_self`, `principal_add_one`, `principal_mul_two`, `isPrincipal_mul_omega`, `principal_mul_iff_mul_left_eq`, `principal_add_omega0`, `principal_mul_omega0_opow_opow`, `principal_opow_omega`, `IsInitial.principal_add`, `principal_add_of_principal_mul_opow`, `isPrincipal_mul_iff_le_two_or_omega0_opow_opow`, `IsInitial.isPrincipal_opow`, `isPrincipal_mul_one`, `isPrincipal_add_mul_of_isPrincipal_add`, `principal_add_omega0_opow`, `isPrincipal_mul_two`, `IsPrincipal.sSup`, `isPrincipal_add_of_le_one`, `isPrincipal_add_omega0_opow`, `isPrincipal_mul_iff_mul_left_eq`, `isPrincipal_add_of_isPrincipal_mul_opow`, `principal_add_opow_of_principal_add`, `principal_swap_iff`, `principal_mul_one`, `isPrincipal_opow_omega`, `principal_iff_of_monotone`, `principal_zero`, `isPrincipal_mul_ord`, `principal_mul_iff_le_two_or_omega0_opow_opow`, `not_isPrincipal_iff_of_monotone`

Submodule

Definitions

Name	Category	Theorems
`IsPrincipal` 📖	CompData	64 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_zorn`, `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`, `NormalizedGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipal`, `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