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	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	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	—	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	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	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike	—	nonempty_fintype Finset.mul_prod_erase Finset.mem_univ Submonoid.coe_mul map_mul mul_assoc surj

---

← Back to Index