Ideal

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

Statistics

Metric	Count
Definitions `mapFrameHom`, `orderEmbedding`, `orderIsoOfPrime`, `primeSpectrumOrderIso`	4
Theorems `algebraMap_mem_map_algebraMap_iff`, `bot_lt_comap_prime`, `coe_primeSpectrumOrderIso_apply_coe_asIdeal`, `coe_primeSpectrumOrderIso_symm_apply_asIdeal`, `comap_le_comap_iff`, `comap_map_of_isPrimary_disjoint`, `comap_map_of_isPrime_disjoint`, `disjoint_comap_iff`, `ideal_eq_iInf_comap_map_away`, `instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul`, `isPrime_iff_isPrime_disjoint`, `isPrime_of_isPrime_disjoint`, `mapFrameHom_apply`, `map_algebraMap_ne_top_iff_disjoint`, `map_comap`, `map_eq_top_of_not_subset`, `map_inf`, `map_radical`, `mem_map_algebraMap_iff`, `mk'_mem_iff`, `mk'_mem_map_algebraMap_iff`, `of_surjective`, `orderIsoOfPrime_apply_coe`, `orderIsoOfPrime_symm_apply_coe`, `surjective_quotientMap_of_maximal_of_localization`, `of_isLocalization`	26
Total	30

IsLocalization

Definitions

Name	Category	Theorems
`mapFrameHom` 📖	CompOp	1 math math: `mapFrameHom_apply`
`orderEmbedding` 📖	CompOp	—
`orderIsoOfPrime` 📖	CompOp	2 math math: `orderIsoOfPrime_symm_apply_coe`, `orderIsoOfPrime_apply_coe`
`primeSpectrumOrderIso` 📖	CompOp	2 math math: `coe_primeSpectrumOrderIso_symm_apply_asIdeal`, `coe_primeSpectrumOrderIso_apply_coe_asIdeal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_mem_map_algebraMap_iff` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.map` `RingHom` `RingHom.instFunLike` `algebraMap` `DFunLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mk'_one` `mk'_mem_map_algebraMap_iff`
`bot_lt_comap_prime` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Bot.bot` `Submodule.instBot` `Ideal.comap` `RingHom` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass`	—	`RingHom.instRingHomClass` `Ideal.comap_bot_of_injective` `injective` `Ideal.isPrime_bot` `IsDomain.toNontrivial` `isDomain_of_le_nonZeroDivisors` `IsDomain.to_noZeroDivisors` `OrderIso.lt_iff_lt` `Ne.bot_lt`
`coe_primeSpectrumOrderIso_apply_coe_asIdeal` 📖	mathematical	—	`SetLike.coe` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.setLike` `PrimeSpectrum.asIdeal` `PrimeSpectrum` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike` `Ideal` `DFunLike.coe` `RelIso` `Preorder.toLE` `PartialOrder.toPreorder` `PrimeSpectrum.instPartialOrder` `RelIso.instFunLike` `primeSpectrumOrderIso` `Set.preimage` `RingHom` `RingHom.instFunLike` `algebraMap`	—	—
`coe_primeSpectrumOrderIso_symm_apply_asIdeal` 📖	mathematical	—	`SetLike.coe` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.setLike` `PrimeSpectrum.asIdeal` `DFunLike.coe` `RelIso` `PrimeSpectrum` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike` `Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `PrimeSpectrum.instPartialOrder` `RelIso.instFunLike` `RelIso.symm` `primeSpectrumOrderIso` `Set.iInter` `Set.instHasSubset` `Set.preimage` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`Set.iInter_congr_Prop`
`comap_le_comap_iff` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.comap` `RingHom` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass`	—	`OrderEmbedding.le_iff_le`
`comap_map_of_isPrimary_disjoint` 📖	mathematical	`Ideal.IsPrimary` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Submonoid.instSetLike` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	`Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass` `Ideal.map`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Set.not_disjoint_iff` `pow_mem` `Submonoid.instSubmonoidClass` `le_antisymm` `RingHom.instRingHomClass` `mem_map_algebraMap_iff` `Ideal.mem_comap` `mul_comm` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `eq_iff_exists` `Submonoid.coe_mul` `mul_assoc` `Ideal.mul_mem_left` `Ideal.isPrimary_iff` `Set.disjoint_left` `Ideal.le_comap_map`
`comap_map_of_isPrime_disjoint` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Submonoid.instSetLike` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	`Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass` `Ideal.map`	—	`comap_map_of_isPrimary_disjoint` `Ideal.IsPrime.isPrimary`
`disjoint_comap_iff` 📖	mathematical	—	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Submonoid.instSetLike` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Ideal.comap` `RingHom` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass`	—	`RingHom.instRingHomClass` `iff_not_comm` `Set.not_disjoint_iff` `Submonoid.one_mem` `Ideal.eq_top_of_isUnit_mem` `map_units`
`ideal_eq_iInf_comap_map_away` 📖	mathematical	`Ideal.span` `CommSemiring.toSemiring` `SetLike.coe` `Finset` `Finset.instSetLike` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`iInf` `Ideal` `CommSemiring.toSemiring` `Submodule.instInfSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Ideal.comap` `Localization.Away` `CommSemiring.toCommMonoid` `RingHom` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `RingHom.instFunLike` `algebraMap` `OreLocalization.instAlgebra` `Algebra.id` `RingHom.instRingHomClass` `Ideal.map`	—	`le_antisymm` `RingHom.instRingHomClass` `Submodule.mem_of_span_eq_top_of_smul_pow_mem` `mem_map_algebraMap_iff` `Localization.isLocalization` `eq_iff_exists` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `pow_add` `mul_assoc` `mul_comm` `Ideal.mul_mem_left`
`instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul` 📖	mathematical	—	`IsDomain` `Localization` `CommRing.toCommMonoid` `Algebra.algebraMapSubmonoid` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal.primeCompl` `OreLocalization.instSemiring` `OreLocalization.oreSetComm`	—	`isDomain_localization` `map_le_nonZeroDivisors_of_injective` `IsDomain.to_noZeroDivisors` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `FaithfulSMul.algebraMap_injective` `Ideal.primeCompl_le_nonZeroDivisors`
`isPrime_iff_isPrime_disjoint` 📖	mathematical	—	`Ideal.IsPrime` `CommSemiring.toSemiring` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`RingHom.instRingHomClass` `Ideal.IsPrime.ne_top` `eq_top_iff` `OrderEmbedding.le_iff_le` `le_of_eq` `Ideal.IsPrime.mem_or_mem` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Ideal.mem_comap` `Set.disjoint_left` `Ideal.eq_top_of_isUnit_mem` `map_units` `exists_mk'_eq` `mk'_mul` `Ideal.IsPrime.mul_mem_iff_mem_or_mem` `Ideal.instIsTwoSided` `mk'_mem_iff`
`isPrime_of_isPrime_disjoint` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Submonoid.instSetLike` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	`Ideal.IsPrime` `CommSemiring.toSemiring` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`RingHom.instRingHomClass` `isPrime_iff_isPrime_disjoint` `comap_map_of_isPrime_disjoint`
`mapFrameHom_apply` 📖	mathematical	—	`DFunLike.coe` `FrameHom` `Ideal` `CommSemiring.toSemiring` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `FrameHom.instFunLike` `mapFrameHom` `Ideal.map` `RingHom` `RingHom.instFunLike` `algebraMap`	—	—
`map_algebraMap_ne_top_iff_disjoint` 📖	mathematical	—	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Submonoid.instSetLike` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `algebraMap_mem_map_algebraMap_iff` `mul_one`
`map_comap` 📖	mathematical	—	`Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `Ideal.comap` `RingHom.instRingHomClass`	—	`le_antisymm` `RingHom.instRingHomClass` `Ideal.map_le_iff_le_comap` `le_rfl` `exists_mk'_eq` `Ideal.mul_mem_right` `Submonoid.LocalizationMap.map_units` `Ideal.instIsTwoSided` `Ideal.mem_map_of_mem` `mk'_spec`
`map_eq_top_of_not_subset` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Compl.compl` `Set.instCompl` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike`	`Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`Ideal.eq_top_of_isUnit_mem` `Ideal.mem_map_of_mem` `map_units`
`map_inf` 📖	mathematical	—	`Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `Ideal` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`le_antisymm` `Ideal.map_inf_le` `RingHom.instRingHomClass` `mem_map_algebraMap_iff` `eq` `Ideal.mul_mem_right` `Ideal.instIsTwoSided` `mul_comm` `mul_assoc` `eq_mk'_iff_mul_eq` `mk'_cancel`
`map_radical` 📖	mathematical	—	`Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `Ideal.radical`	—	`LE.le.antisymm` `Ideal.map_radical_le` `RingHom.instRingHomClass` `exists_mk'_eq` `mk'_mem_map_algebraMap_iff` `Submonoid.instSubmonoidClass` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Ideal.mul_mem_left`
`mem_map_algebraMap_iff` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.map` `RingHom` `RingHom.instFunLike` `algebraMap` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe`	—	`Ideal.mem_sInf` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_one` `Ideal.unit_mul_mem_iff_mem` `map_units` `mul_comm` `Ideal.mem_map_of_mem`
`mk'_mem_iff` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `mk'` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`mk'_spec` `mul_comm` `Ideal.mul_mem_left` `isUnit_iff_exists_inv` `instIsDedekindFiniteMonoid` `map_units` `mul_one` `mul_assoc`
`mk'_mem_map_algebraMap_iff` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.map` `RingHom` `RingHom.instFunLike` `algebraMap` `mk'` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Ideal.unit_mul_mem_iff_mem` `map_units` `mk'_spec'` `mem_map_algebraMap_iff` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `eq_iff_exists` `mul_comm` `Ideal.mul_mem_left` `one_mul`
`of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `RingHom.comp` `algebraMap` `Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom.instRingHomClass` `Ideal.map`	`IsLocalization` `CommRing.toCommSemiring` `Submonoid.map` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`	—	`RingHom.instRingHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `IsUnit.map` `map_units` `surj` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `DFunLike.congr_arg` `mk'_mem_map_algebraMap_iff` `mk'_one` `RingHom.comp_apply` `map_sub` `RingHomClass.toAddMonoidHomClass` `sub_eq_zero` `mul_sub`
`orderIsoOfPrime_apply_coe` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Ideal.IsPrime` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Submonoid.instSetLike` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `RelIso` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `RelIso.instFunLike` `orderIsoOfPrime` `Ideal.comap` `RingHom` `RingHom.instFunLike` `algebraMap`	—	—
`orderIsoOfPrime_symm_apply_coe` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Ideal.IsPrime` `DFunLike.coe` `RelIso` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Submonoid.instSetLike` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `RelIso.instFunLike` `RelIso.symm` `orderIsoOfPrime` `Ideal.map` `RingHom` `RingHom.instFunLike` `algebraMap`	—	—
`surjective_quotientMap_of_maximal_of_localization` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.comap` `RingHom` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass`	`HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `Ideal.quotientMap` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`RingHom.instRingHomClass` `Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_surjective` `exists_mk'_eq` `Ideal.eq_top_iff_one` `mk'_eq_mul_mk'_one` `mk'_self` `Ideal.mul_mem_right` `Ideal.mem_comap` `Ideal.Quotient.eq_zero_iff_mem` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `IsField.mul_inv_cancel` `Ideal.Quotient.maximal_ideal_iff_isField_quotient` `le_rfl` `sub_eq_zero` `map_sub` `RingHomClass.toAddMonoidHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `Ideal.Quotient.isDomain` `mul_left_cancel₀` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass`

Module.IsTorsionFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isLocalization` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`Module.IsTorsionFree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`Submonoid.map_le_of_le_comap` `LE.le.trans` `nonZeroDivisors_le_comap_nonZeroDivisors_of_injective` `IsDomain.to_noZeroDivisors` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `FaithfulSMul.algebraMap_injective` `to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IsLocalization.isDomain_of_le_nonZeroDivisors` `Submonoid.le_comap_map` `MonoidWithZeroHomClass.toMonoidHomClass` `IsLocalization.ringHom_ext` `IsLocalization.map_comp` `Module.isTorsionFree_iff_algebraMap_injective` `RingHom.injective_iff_ker_eq_bot` `RingHom.ker_eq_bot_iff_eq_zero` `IsLocalization.exists_mk'_eq` `IsLocalization.map_mk'` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `injective_iff_map_eq_zero'` `RingHomClass.toAddMonoidHomClass`

---

← Back to Index