Lemmas

📁 Source: Mathlib/RingTheory/Localization/Away/Lemmas.lean

Statistics

Metric	Count
Definitions mulNumerator	1
Theorems quotient_of_isIdempotentElem, span_range_mulNumerator_eq_top	2
Total	3

IsLocalization.Away

Definitions

Name	Category	Theorems
mulNumerator 📖	CompOp	1 math math: span_range_mulNumerator_eq_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quotient_of_isIdempotentElem 📖	mathematical	IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	IsLocalization.Away CommRing.toCommSemiring HasQuotient.Quotient Ideal CommSemiring.toSemiring Ideal.instHasQuotient_1 Ideal.span Set Set.instSingletonSet SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ideal.Quotient.commSemiring Ideal.instAlgebraQuotient Algebra.id	—	IsLocalization.away_of_isIdempotentElem Ideal.mk_ker Ideal.instIsTwoSided_1 Quotient.mk_surjective
span_range_mulNumerator_eq_top 📖	mathematical	Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalization.Away Set Set.instMembership	Set.range Set.Elem mulNumerator	—	Ideal.radical_eq_top eq_top_iff Ideal.span_le SetLike.mem_coe IsLocalization.mem_span_map Ideal.subset_span IsLocalization.eq_mk'_iff_mul_eq map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass pow_add mul_assoc sec_spec mul_comm pow_one IsLocalization.mk'_one map_one MonoidHomClass.toOneHomClass IsLocalization.eq mul_one one_mul Ideal.mul_mem_left

---

← Back to Index