Pi

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

Statistics

Metric	Count
Definitions	0
Theorems algebraMap_pi_surjective_of_isLocalization, bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom, iff_map_piEvalRingHom, instForallPiUniv, isUnit_piRingHom_algebraMap_comp_piEvalRingHom, surjective_piRingHom_algebraMap_comp_piEvalRingHom	6
Total	6

IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_pi_surjective_of_isLocalization 📖	mathematical	Ring.KrullDimLE IsLocalRing CommSemiring.toSemiring	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.commSemiring RingHom.instFunLike algebraMap	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass isUnit_piRingHom_algebraMap_comp_piEvalRingHom Localization.isLocalization surjective_piRingHom_algebraMap_comp_piEvalRingHom Function.Bijective.injective bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom lift_eq
bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom 📖	mathematical	IsLocalization Submonoid.map Pi.mulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom Pi.nonAssocSemiring RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Pi.evalRingHom	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.commSemiring RingHom.instFunLike lift Pi.ringHom Pi.nonAssocSemiring RingHom.comp algebraMap Pi.evalRingHom isUnit_piRingHom_algebraMap_comp_piEvalRingHom	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass iff_map_piEvalRingHom instForallPiUniv RingEquiv.bijective Submonoid.map_equiv_eq_comap_symm
iff_map_piEvalRingHom 📖	mathematical	—	IsLocalization Pi.commSemiring Submonoid.pi MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Set.univ Submonoid.map Pi.mulOneClass RingHom Pi.nonAssocSemiring RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Pi.evalRingHom	—	iff_of_le_of_exists_dvd MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass prod_mem Submonoid.instSubmonoidClass pi_dvd_iff Fintype.prod_apply Dvd.dvd.trans Eq.dvd Finset.dvd_prod_of_mem Finset.mem_univ
instForallPiUniv 📖	mathematical	IsLocalization	IsLocalization Pi.commSemiring Submonoid.pi MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Set.univ Pi.instAlgebraForall	—	Pi.isUnit_iff map_units surj exists_of_eq
isUnit_piRingHom_algebraMap_comp_piEvalRingHom 📖	mathematical	IsLocalization Submonoid.map Pi.mulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom Pi.nonAssocSemiring RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Pi.evalRingHom	IsUnit Pi.monoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Pi.nonAssocSemiring Semiring.toNonAssocSemiring RingHom.instFunLike Pi.ringHom RingHom.comp algebraMap Pi.evalRingHom Submonoid Pi.mulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Pi.isUnit_iff map_units
surjective_piRingHom_algebraMap_comp_piEvalRingHom 📖	mathematical	IsLocalization Submonoid.map Pi.mulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom Pi.nonAssocSemiring RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Pi.evalRingHom Ring.KrullDimLE IsLocalRing	DFunLike.coe RingHom Pi.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike Pi.ringHom RingHom.comp algebraMap Pi.evalRingHom	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Function.Surjective.piMap Function.surjective_to_subsingleton Nontrivial.to_nonempty IsLocalRing.toNontrivial Unique.instSubsingleton AlgEquiv.surjective

---

← Back to Index