DedekindDomain

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

Statistics

Metric	Count
Definitions	0
Theorems exists_isInternal_prime_power_torsion, isInternal_prime_power_torsion, isInternal_prime_power_torsion_of_is_torsion_by_ideal	3
Total	3

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isInternal_prime_power_torsion 📖	mathematical	Module.IsTorsion CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	DirectSum.IsInternal Ideal Finset SetLike.instMembership Finset.instSetLike Submodule setLike addSubmonoidClass torsionBySet SetLike.coe NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule instPowNat IsScalarTower.right Algebra.id	—	addSubmonoidClass IsScalarTower.right Ideal.uniqueFactorizationMonoid UniqueFactorizationMonoid.prime_of_factor Multiset.mem_toFinset isInternal_prime_power_torsion
isInternal_prime_power_torsion 📖	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 annihilator Top.top Submodule instTop setLike addSubmonoidClass torsionBySet SetLike.coe NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule instPowNat IsScalarTower.right Algebra.id Multiset.count	—	Module.isTorsionBySet_annihilator_top annihilator_top_inter_nonZeroDivisors isInternal_prime_power_torsion_of_is_torsion_by_ideal ne_bot_iff nonZeroDivisors.ne_zero IsDomain.toNontrivial
isInternal_prime_power_torsion_of_is_torsion_by_ideal 📖	mathematical	Module.IsTorsionBySet CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.coe Ideal setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	DirectSum.IsInternal Finset SetLike.instMembership Finset.instSetLike Multiset.toFinset UniqueFactorizationMonoid.factors CommSemiring.toCommMonoidWithZero IdemCommSemiring.toCommSemiring Ideal.instIdemCommSemiring Ideal.uniqueFactorizationMonoid Submodule addSubmonoidClass torsionBySet instPowNat IsScalarTower.right Algebra.id Multiset.count	—	Ideal.uniqueFactorizationMonoid UniqueFactorizationMonoid.prime_of_factor Multiset.mem_toFinset torsionBySet_isInternal IsScalarTower.right irreducible_pow_sup Ideal.zero_eq_bot pow_ne_zero isReduced_of_noZeroDivisors Ideal.instNoZeroDivisors IsDomain.to_noZeroDivisors Prime.ne_zero Prime.irreducible Ideal.isCancelMulZero Multiset.count_eq_zero UniqueFactorizationMonoid.normalizedFactors_of_irreducible_pow Multiset.mem_replicate normalize_eq Unique.instSubsingleton zero_min Nat.instCanonicallyOrderedAdd pow_zero Ideal.one_eq_top Finset.inf_eq_iInf IsDedekindDomain.inf_prime_pow_eq_prod Finset.prod_multiset_count associated_iff_eq UniqueFactorizationMonoid.factors_prod

---

← Back to Index