Lemmas

📁 Source: Mathlib/GroupTheory/MonoidLocalization/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems pi, surj_pi_of_finite, pi, surj_pi_of_finite	4
Total	4

AddSubmonoid.IsLocalizationMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi 📖	mathematical	AddSubmonoid.IsLocalizationMap	AddSubmonoid.IsLocalizationMap Pi.addCommMonoid AddSubmonoid.pi AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Set.univ Pi.map	—	Pi.isAddUnit_iff map_addUnits surj exists_of_eq
surj_pi_of_finite 📖	mathematical	AddSubmonoid.IsLocalizationMap DFunLike.coe	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike AddZero.toAdd AddZeroClass.toAddZero DFunLike.coe	—	nonempty_fintype Finset.add_sum_erase Finset.mem_univ AddSubmonoid.coe_add map_add add_assoc surj

Submonoid.IsLocalizationMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi 📖	mathematical	Submonoid.IsLocalizationMap	Submonoid.IsLocalizationMap Pi.commMonoid Submonoid.pi Monoid.toMulOneClass CommMonoid.toMonoid Set.univ Pi.map	—	Pi.isUnit_iff map_units surj exists_of_eq
surj_pi_of_finite 📖	mathematical	Submonoid.IsLocalizationMap DFunLike.coe	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike MulOne.toMul MulOneClass.toMulOne DFunLike.coe	—	nonempty_fintype Finset.mul_prod_erase Finset.mem_univ Submonoid.coe_mul map_mul mul_assoc surj

---

← Back to Index