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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Ideal.instHasQuotient_1 AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid Ideal.span Set Set.instSingletonSet SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidAlgebra.ring CommRing.toRing AddMonoidAlgebra.instMul Finsupp.instAdd AddMonoid.toAddZeroClass RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass RingHom.instFunLike MvPolynomial.C MvPolynomial.X AddMonoidAlgebra.zero Finsupp.instZero Ideal.Quotient.semiring Ideal.instAlgebraQuotient AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid 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 AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass C algebraMvPolynomial	—	instIsScalarTower isLocalizedModule_iff_isLocalization AddMonoidAlgebra.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 AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike C IsLocalization.mk' AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid 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