Reduced

📁 Source: Mathlib/RingTheory/LocalProperties/Reduced.lean

Statistics

Metric	Count
Definitions Reduced	1
Theorems instIsReducedLocalization, isReduced_localizationPreserves, isReduced_ofLocalizationMaximal	3
Total	4

Monoid.PushoutI

Definitions

Name	Category	Theorems
Reduced 📖	MathDef	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsReducedLocalization 📖	mathematical	—	IsReduced Localization CommRing.toCommMonoid OreLocalization.instZero CommMonoid.toMonoid OreLocalization.oreSetComm MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toMulAction Monoid.toNatPow OreLocalization.instMonoid	—	isReduced_localizationPreserves Localization.isLocalization
isReduced_localizationPreserves 📖	mathematical	—	LocalizationPreserves IsReduced MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	pow_zero one_mul MulZeroClass.zero_mul IsLocalization.surj IsLocalization.eq_iff_exists RingHom.map_zero mul_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsNilpotent.eq_zero pow_succ' mul_left_comm MulZeroClass.mul_zero mul_assoc IsLocalization.map_units IsLocalization.map_eq_zero_iff mul_comm
isReduced_ofLocalizationMaximal 📖	mathematical	—	OfLocalizationMaximal IsReduced MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	eq_zero_of_localization IsNilpotent.eq_zero Ideal.IsMaximal.isPrime' IsNilpotent.map RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass

---

← Back to Index