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 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 Pi.commSemiring lift Pi.ringHom RingHom.comp algebraMap 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	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 DFunLike.coe Pi.ringHom RingHom.comp algebraMap Submonoid 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 Pi.ringHom RingHom.comp algebraMap	—	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