Localization

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

Statistics

Metric	Count
Definitions mvPolynomialQuotientEquiv	1
Theorems mvPolynomialQuotientEquiv_apply, isLocalization, isLocalization_C_mk'	3
Total	4

IsLocalization.Away

Definitions

Name	Category	Theorems
mvPolynomialQuotientEquiv 📖	CompOp	1 math math: mvPolynomialQuotientEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mvPolynomialQuotientEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv HasQuotient.Quotient MvPolynomial CommRing.toCommSemiring Ideal CommSemiring.toSemiring MvPolynomial.commSemiring Ideal.instHasQuotient_1 MvPolynomial.instCommRingMvPolynomial Ideal.span Set Set.instSingletonSet SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.C MvPolynomial.X AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ideal.Quotient.semiring Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id AlgEquiv.instFunLike mvPolynomialQuotientEquiv Ring.toSemiring Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 AlgHom AlgHom.funLike MvPolynomial.aeval invSelf	—	Ideal.instIsTwoSided_1

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalization 📖	mathematical	—	IsLocalization MvPolynomial CommRing.toCommSemiring commSemiring Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass C algebraMvPolynomial	—	instIsScalarTower isLocalizedModule_iff_isLocalization isScalarTower IsScalarTower.right isLocalizedModule_iff_isBaseChange IsBaseChange.of_equiv Algebra.to_smulCommClass RingHomInvPair.ids algebraTensorAlgEquiv_tmul one_smul
isLocalization_C_mk' 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C IsLocalization.mk' Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMvPolynomial isLocalization Submonoid SetLike.instMembership Submonoid.instSetLike Submonoid.mem_map_of_mem	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass isLocalization Submonoid.mem_map_of_mem map_C NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass IsLocalization.mk'_spec

---

← Back to Index