PID

📁 Source: Mathlib/Algebra/Module/PID.lean

Statistics

Metric	Count
Definitions	0
Theorems torsionOf_eq_span_pow_pOrder, equiv_directSum_of_isTorsion, equiv_free_prod_directSum, exists_ker_toSpanSingleton_eq_annihilator, exists_smul_eq_zero_and_mk_eq, p_pow_smul_lift, torsion_by_prime_power_decomposition, exists_isInternal_prime_power_torsion_of_pid, isInternal_prime_power_torsion_of_pid, isSemisimple_torsionBy_of_irreducible	10
Total	10

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
torsionOf_eq_span_pow_pOrder 📖	mathematical	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.IsTorsion' AddCommGroup.toAddCommMonoid Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.powers Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction	torsionOf span Set Set.instSingletonSet Monoid.toNatPow Submodule.pOrder AddCommMonoid.toAddMonoid	—	IsPrincipalIdealRing.principal span_singleton_generator span_singleton_eq_span_singleton Associates.mk_eq_mk_iff_associated Associates.mk_pow Submodule.IsPrincipal.mem_iff_generator_dvd Submodule.isTorsion'_powers_iff Lean.Meta.FastSubsingleton.elim Lean.Meta.instFastSubsingletonForall Lean.Meta.instFastSubsingletonDecidable Associates.eq_pow_find_of_dvd_irreducible_pow PrincipalIdealRing.to_uniqueFactorizationMonoid

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv_directSum_of_isTorsion 📖	mathematical	IsTorsion CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum HasQuotient.Quotient Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Ideal.instHasQuotient_1 Submodule.span Set Set.instSingletonSet Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.commRing instAddCommMonoidDirectSum DirectSum.instModule Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup	—	Submodule.addSubmonoidClass RingHomInvPair.ids Submodule.exists_isInternal_prime_power_torsion_of_pid torsion_by_prime_power_decomposition Submodule.isTorsion'_powers_iff Submodule.smul_torsionBy IsNoetherian.finite isNoetherian_submodule' isNoetherian_of_isNoetherianRing_of_finite IsDedekindRing.toIsNoetherian IsDedekindDomain.toIsDedekindRing IsPrincipalIdealRing.isDedekindDomain RingHomCompTriple.ids
equiv_free_prod_directSum 📖	mathematical	—	LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DirectSum HasQuotient.Quotient Submodule NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Ideal.instHasQuotient_1 Submodule.span Set Set.instSingletonSet Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.commRing AddCommGroup.toAddCommMonoid Prod.instAddCommMonoid Finsupp.instAddCommMonoid instAddCommMonoidDirectSum Prod.instModule Finsupp.module DirectSum.instModule Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup	—	RingHomInvPair.ids equiv_directSum_of_isTorsion IsNoetherian.finite isNoetherian_submodule' isNoetherian_of_isNoetherianRing_of_finite IsDedekindRing.toIsNoetherian IsDedekindDomain.toIsDedekindRing IsPrincipalIdealRing.isDedekindDomain Submodule.torsion_isTorsion Finite.quotient Submodule.QuotientTorsion.instIsTorsionFree RingHomCompTriple.ids projective_lifting_property Projective.of_free free_of_finite_type_torsion_free' Submodule.mkQ_surjective Submodule.injective_subtype RingHomSurjective.ids Submodule.range_subtype Submodule.ker_mkQ
exists_ker_toSpanSingleton_eq_annihilator 📖	mathematical	—	LinearMap.ker CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Semiring.toModule RingHom.id LinearMap.toSpanSingleton annihilator	—	RingHomInvPair.ids equiv_free_prod_directSum Finite.of_fintype le_antisymm mul_one smul_eq_mul LinearEquiv.annihilator_eq annihilator_prod annihilator_eq_top_iff Unique.instSubsingleton Fin.isEmpty' annihilator_dfinsupp top_inf_eq Ideal.annihilator_quotient Ideal.instIsTwoSided_1 map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass DFinsupp.ext_iff Finsupp.ext_iff LinearEquiv.map_eq_zero_iff map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearMap.toSpanSingleton_apply LinearMap.mem_ker mem_annihilator
exists_smul_eq_zero_and_mk_eq 📖	mathematical	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring IsTorsion' AddCommGroup.toAddCommMonoid Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.powers Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul toDistribMulAction IsTorsionBy Monoid.toNatPow Submodule.pOrder AddCommMonoid.toAddMonoid	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CommRing.toRing Submodule.span Set Set.instSingletonSet DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring HasQuotient.Quotient Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Ideal.instHasQuotient_1 Submodule.hasQuotient Ideal.Quotient.commRing Submodule.Quotient.addCommGroup Submodule.Quotient.module Ring.toAddCommGroup LinearMap.instFunLike Ideal.Quotient.one	—	Submodule.Quotient.mk_surjective Submodule.Quotient.mk_eq_zero IsScalarTower.left Submodule.Quotient.mk_smul LinearMap.map_smul smul_eq_mul mul_one Submodule.mem_span_singleton_self LinearMap.map_zero p_pow_smul_lift smul_sub sub_eq_zero Submodule.Quotient.mk_sub smul_zero sub_zero
p_pow_smul_lift 📖	—	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring IsTorsion' AddCommGroup.toAddCommMonoid Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.powers Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul toDistribMulAction IsTorsionBy Monoid.toNatPow Submodule.pOrder AddCommMonoid.toAddMonoid Submodule Submodule.setLike Submodule.span Set Set.instSingletonSet	—	—	RingHomInvPair.ids RingHomCompTriple.ids pow_add Ideal.torsionOf_eq_span_pow_pOrder Ideal.instIsTwoSided_1 Ideal.Quotient.torsionBy_eq_span_singleton mem_nonZeroDivisors_of_ne_zero IsDomain.to_noZeroDivisors pow_ne_zero isReduced_of_noZeroDivisors Irreducible.ne_zero Submodule.mem_torsionBy_iff LinearEquiv.map_smul IsScalarTower.left Submodule.coe_smul_of_tower Submodule.coe_zero smul_smul LinearEquiv.map_zero Submodule.mem_span_singleton mul_comm Submodule.Quotient.mk_smul LinearEquiv.eq_symm_apply zero_smul smul_zero LT.lt.le SemigroupAction.mul_smul
torsion_by_prime_power_decomposition 📖	mathematical	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring IsTorsion' AddCommGroup.toAddCommMonoid Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.powers Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul toDistribMulAction	LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum HasQuotient.Quotient Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Ideal.instHasQuotient_1 Submodule.span Set Set.instSingletonSet Monoid.toNatPow Ideal.Quotient.commRing instAddCommMonoidDirectSum DirectSum.instModule Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup	—	RingHomInvPair.ids Finite.exists_fin Unique.instSubsingleton Submodule.mem_bot Submodule.span_empty Set.range_eq_empty Fin.isEmpty' Submodule.mem_top Submodule.exists_isTorsionBy Function.Surjective.forall Submodule.Quotient.mk_surjective Submonoid.isScalarTower IsScalarTower.left Submodule.Quotient.mk_smul Submodule.Quotient.mk_zero RingHomSurjective.ids Function.comp_assoc Set.range_comp Fin.range_succAbove Submodule.span_insert_zero Submodule.Quotient.mk_eq_zero Submodule.mem_span_singleton_self Set.insert_image_compl_eq_range Set.image_congr Submodule.range_mkQ Submodule.map_top Submodule.map_span RingHomCompTriple.ids exists_smul_eq_zero_and_mk_eq LinearEquiv.apply_symm_apply Submodule.injective_subtype Submodule.range_subtype LinearEquiv.ker_comp Submodule.ker_mkQ LinearMap.comp_assoc DirectSum.linearMap_ext Submodule.linearMap_qext LinearMap.ext_ring LinearEquiv.coe_toLinearMap LinearMap.id_apply DirectSum.toModule_lof Submodule.liftQSpanSingleton_apply LinearMap.toSpanSingleton_apply_one Ideal.instIsTwoSided_1 map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Ideal.torsionOf_eq_span_pow_pOrder

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isInternal_prime_power_torsion_of_pid 📖	mathematical	Module.IsTorsion CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	DirectSum.IsInternal Submodule setLike addSubmonoidClass torsionBy Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	addSubmonoidClass Ideal.uniqueFactorizationMonoid IsPrincipalIdealRing.isDedekindDomain IsPrincipalIdealRing.principal UniqueFactorizationMonoid.prime_of_factor Multiset.mem_toFinset Prime.irreducible IsDomain.toIsCancelMulZero IsPrincipal.prime_generator_of_isPrime Ideal.isPrime_of_prime Prime.ne_zero isInternal_prime_power_torsion_of_pid
isInternal_prime_power_torsion_of_pid 📖	mathematical	Module.IsTorsion CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	DirectSum.IsInternal Ideal Finset SetLike.instMembership Finset.instSetLike Multiset.toFinset UniqueFactorizationMonoid.factors CommSemiring.toCommMonoidWithZero IdemCommSemiring.toCommSemiring Ideal.instIdemCommSemiring Ideal.uniqueFactorizationMonoid IsPrincipalIdealRing.isDedekindDomain annihilator Top.top Submodule instTop setLike addSubmonoidClass torsionBy Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsPrincipal.generator NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsPrincipalIdealRing.principal Multiset.count	—	Ideal.uniqueFactorizationMonoid IsPrincipalIdealRing.isDedekindDomain addSubmonoidClass IsPrincipalIdealRing.principal IsScalarTower.right torsionBySet_span_singleton_eq Ideal.submodule_span_eq IsScalarTower.left Ideal.span_singleton_pow Ideal.instIsTwoSided_1 Ideal.span_singleton_generator isInternal_prime_power_torsion
isSemisimple_torsionBy_of_irreducible 📖	mathematical	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	IsSemisimpleModule CommRing.toRing Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership setLike torsionBy addCommGroup module	—	isSemisimpleModule_iff OrderIso.complementedLattice complementedLattice PrincipalIdealRing.isMaximal_of_irreducible

---

← Back to Index