PID

📁 Source: Mathlib/RingTheory/DedekindDomain/PID.lean

Statistics

Metric	Count
Definitions	0
Theorems of_finite_maximals_of_inv, isPrincipal_of_unit_of_comap_mul_span_singleton_eq_top, of_finite_maximals_of_isUnit, eq_span_singleton_of_mem_of_notMem_sq_of_notMem_prime_ne, isPrincipalIdealRing_localization_over_prime, mem_normalizedFactors_of_isPrime, of_finite_maximals, of_finite_primes, of_isDedekindDomain_of_uniqueFactorizationMonoid	9
Total	9

FractionalIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrincipal_of_unit_of_comap_mul_span_singleton_eq_top 📖	mathematical	FractionalIdeal SetLike.instMembership instSetLike Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring Units Units.instInv Submodule.comap CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule RingHom.id Algebra.linearMap Submodule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule.mul IsScalarTower.right coeToSubmodule Submodule.span Set Set.instSingletonSet Top.top Submodule.instTop	Submodule.IsPrincipal	—	IsScalarTower.right Units.mul_inv Submodule.map_comap_eq_self RingHomSurjective.ids Submodule.one_eq_range coe_one coe_mul coe_ext_iff le_imp_le_of_le_of_le mul_le_mul_right Submodule.instMulLeftMono Submodule.span_singleton_le_iff_mem le_refl IsLocalization.coeSubmodule_top Submodule.mem_one RingHom.map_one Submodule.mem_mul_span_singleton coe_spanSingleton inv_inv Units.eq_inv_of_mul_eq_one_left le_antisymm mul_comm instMulLeftMono spanSingleton_le_iff_mem one_le mul_mem_mul mem_spanSingleton_self

FractionalIdeal.isPrincipal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_finite_maximals_of_inv 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero FractionalIdeal FractionalIdeal.instMul FractionalIdeal.instOne	Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule FractionalIdeal.coeToSubmodule	—	Set.Finite.mem_toFinset Ideal.IsMaximal.coprime_of_ne left_lt_sup LT.lt.trans_eq Ne.lt_top Ideal.IsMaximal.ne_top Ideal.sup_iInf_eq_top Ideal.instIsTwoSided_1 IsScalarTower.right SetLike.exists_of_lt instIsConcreteLE IsLocalization.coeSubmodule_strictMono FractionalIdeal.coe_mul FractionalIdeal.coe_ext_iff Submodule.mul_le Mathlib.Tactic.Push.not_and_eq Submodule.sum_mem Submodule.smul_mem FractionalIdeal.isPrincipal_of_unit_of_comap_mul_span_singleton_eq_top instIsDedekindFiniteMonoid of_not_not Ideal.exists_le_maximal Eq.le Submodule.mul_mem_mul IsLocalization.coeSubmodule_mono Submodule.mem_span_singleton_self map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Algebra.smul_def Submodule.add_mem_iff_left Finset.mem_erase Submodule.mem_map_of_mem RingHomSurjective.ids Ideal.mul_mem_right Finset.add_sum_erase Finset.sum_congr mul_smul_comm Algebra.to_smulCommClass Finset.mul_sum Ideal.IsPrime.mem_or_mem Ideal.IsMaximal.isPrime IsLocalization.injective Zero.instNonempty SetLike.not_le_iff_exists Function.sometimes_spec

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_span_singleton_of_mem_of_notMem_sq_of_notMem_prime_ne 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id	span Set Set.instSingletonSet	—	ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass span_singleton_eq_bot mem_bot span_singleton_le_iff_mem associated_iff_eq Unique.instSubsingleton uniqueFactorizationMonoid UniqueFactorizationMonoid.associated_iff_normalizedFactors_eq_normalizedFactors le_antisymm UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors IsScalarTower.right dvd_iff_le UniqueFactorizationMonoid.normalizedFactors_irreducible Prime.irreducible isCancelMulZero prime_of_isPrime normalize_eq Multiset.count_singleton Eq.le count_normalizedFactors_eq pow_one pow_zero one_eq_top zero_add Multiset.count_eq_zero isPrime_of_prime irreducible_iff_prime UniqueFactorizationMonoid.instDecompositionMonoid UniqueFactorizationMonoid.irreducible_of_normalized_factor

Ideal.IsPrincipal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_finite_maximals_of_isUnit 📖	mathematical	IsUnit 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	Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	IsLocalization.coeSubmodule_isPrincipal Localization.isLocalization le_rfl FractionalIdeal.isPrincipal.of_finite_maximals_of_inv Units.mul_inv

IsDedekindDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrincipalIdealRing_localization_over_prime 📖	mathematical	—	IsPrincipalIdealRing CommSemiring.toSemiring CommRing.toCommSemiring	—	IsPrincipalIdealRing.of_finite_primes Set.Finite.ofFinset Ideal.uniqueFactorizationMonoid Finset.mem_filter Finset.mem_union Finset.mem_singleton Set.mem_setOf Multiset.mem_toFinset IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime

IsLocalization.OverPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_normalizedFactors_of_isPrime 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Multiset Multiset.instMembership UniqueFactorizationMonoid.normalizedFactors CommSemiring.toCommMonoidWithZero IdemCommSemiring.toCommSemiring Ideal.instIdemCommSemiring Ideal.normalizationMonoid Ideal.uniqueFactorizationMonoid Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	map_le_nonZeroDivisors_of_injective IsDomain.to_noZeroDivisors RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass FaithfulSMul.algebraMap_injective Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDedekindDomain.toIsDomain IsDomain.toNontrivial Ideal.primeCompl_le_nonZeroDivisors Ideal.uniqueFactorizationMonoid IsLocalization.isDomain_of_local_atPrime IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain Localization.isLocalization Localization.AtPrime.isLocalRing Submodule.ne_bot_iff IsLocalization.AtPrime.isLocalRing IsLocalization.AtPrime.to_map_mem_maximal_iff IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors mem_nonZeroDivisors_of_ne_zero Multiset.singleton_le Unique.instSubsingleton normalize_eq UniqueFactorizationMonoid.normalizedFactors_irreducible Prime.irreducible Ideal.isCancelMulZero Ideal.prime_of_isPrime UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors Ideal.zero_eq_bot Ideal.map_eq_bot_iff_of_injective IsScalarTower.algebraMap_eq IsLocalization.injective IsScalarTower.right Ideal.dvd_iff_le IsScalarTower.of_algebraMap_eq IsScalarTower.algebraMap_apply Submonoid.le_comap_map MonoidWithZeroHomClass.toMonoidHomClass IsLocalization.map_eq Ideal.map_map Localization.AtPrime.map_eq_maximalIdeal Ideal.map_le_iff_le_comap Ideal.IsMaximal.isPrime IsLocalRing.maximalIdeal.isMaximal isIntegral_localization Algebra.IsIntegral.of_finite Ideal.eq_bot_of_comap_eq_bot IsLocalRing.toNontrivial Ideal.comap_isPrime le_refl

IsPrincipalIdealRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_finite_maximals 📖	mathematical	—	IsPrincipalIdealRing CommSemiring.toSemiring CommRing.toCommSemiring	—	eq_or_ne bot_isPrincipal Ideal.IsPrincipal.of_finite_maximals_of_isUnit IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid IsDedekindDomain.toIsDomain Localization.isLocalization FractionalIdeal.coe_ideal_mul_inv
of_finite_primes 📖	mathematical	—	IsPrincipalIdealRing CommSemiring.toSemiring CommRing.toCommSemiring	—	of_finite_maximals Set.Finite.subset Ideal.IsMaximal.isPrime
of_isDedekindDomain_of_uniqueFactorizationMonoid 📖	mathematical	—	IsPrincipalIdealRing CommSemiring.toSemiring CommRing.toCommSemiring	—	of_prime_ne_bot Ideal.IsPrime.exists_mem_prime_of_ne_bot Ideal.span_singleton_prime Prime.ne_zero Ring.DimensionLeOne.prime_le_prime_iff_eq IsDedekindDomainDvr.ring_dimensionLEOne IsDedekindDomain.toIsDomain IsDedekindDomain.isDedekindDomainDvr Ideal.span_singleton_le_iff_mem instIsPrincipalSpanSingletonSet

---

← Back to Index