MonoidWithZero

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

Statistics

Metric	Count
Definitions instCommMonoidWithZero, MonoidWithZero, lift₀	3
Theorems liftOn_zero, mk_zero, map_zero, isCancelMulZero, lift₀_apply, lift₀_def, map_eq_zero_iff, map_nonZeroDivisors_le, map_zero, mk'_eq_zero_iff, mk'_zero, noZeroDivisors, nonZeroDivisors_le_comap, nontrivial, sec_zero_fst, subsingleton, subsingleton_iff, instMonoidWithZeroHomClassLocalizationMap	18
Total	21

Localization

Definitions

Name	Category	Theorems
instCommMonoidWithZero 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
liftOn_zero 📖	mathematical	—	liftOn CommMonoidWithZero.toCommMonoid Localization OreLocalization.instZero CommMonoid.toMonoid OreLocalization.oreSetComm MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero Monoid.toMulAction Submonoid MulZeroOneClass.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.one	—	mk_zero
mk_zero 📖	mathematical	—	CommMonoidWithZero.toCommMonoid MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero Localization OreLocalization.instZero CommMonoid.toMonoid OreLocalization.oreSetComm Monoid.toMulAction	—	OreLocalization.zero_oreDiv'

Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMonoidWithZeroHomClassLocalizationMap 📖	mathematical	—	MonoidWithZeroHomClass LocalizationMap CommMonoidWithZero.toCommMonoid MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LocalizationMap.instFunLike	—	LocalizationMap.instMonoidHomClass LocalizationMap.surj MulZeroClass.zero_mul map_mul MonoidHomClass.toMulHomClass MulZeroClass.mul_zero

Submonoid.IsLocalizationMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_zero 📖	mathematical	Submonoid.IsLocalizationMap CommMonoidWithZero.toCommMonoid DFunLike.coe	MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	Submonoid.LocalizationMap.map_zero

Submonoid.LocalizationMap

Definitions

Name	Category	Theorems
lift₀ 📖	CompOp	2 math math: lift₀_apply, lift₀_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCancelMulZero 📖	mathematical	—	IsCancelMulZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MulZeroClass.toZero	—	Commute.isRegular_iff Commute.all Commute.isRightRegular_iff surj IsRightRegular.of_mul IsRegular.right map_isRegular isCancelMulZero_iff_forall_isRegular IsUnit.mul_left_eq_zero map_units map_zero MonoidWithZeroHomClass.toZeroHomClass Submonoid.instMonoidWithZeroHomClassLocalizationMap
lift₀_apply 📖	mathematical	IsUnit MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike Submonoid MulZeroOneClass.toMulOneClass SetLike.instMembership Submonoid.instSetLike	lift₀ MulZeroClass.toMul MulZeroOneClass.toMulZeroClass Monoid.toMulOneClass CommMonoid.toMonoid CommMonoidWithZero.toCommMonoid sec Units.val Units Units.instInv MonoidHom MulOneClass.toMulOne Submonoid.toMonoid Units.instMulOneClass MonoidHom.instFunLike IsUnit.liftRight MonoidHom.restrict Submonoid.instSubmonoidClass MonoidWithZeroHom.toMonoidHom	—	—
lift₀_def 📖	mathematical	IsUnit MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike Submonoid MulZeroOneClass.toMulOneClass SetLike.instMembership Submonoid.instSetLike	lift₀ MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid CommMonoidWithZero.toCommMonoid MonoidHom.instFunLike lift MonoidHomClass.toMonoidHom MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass	—	—
map_eq_zero_iff 📖	mathematical	—	DFunLike.coe Submonoid.LocalizationMap CommMonoidWithZero.toCommMonoid instFunLike MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MulZeroClass.toMul Submonoid MulZeroOneClass.toMulOneClass SetLike.instMembership Submonoid.instSetLike	—	map_zero MulZeroClass.mul_zero
map_nonZeroDivisors_le 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Submonoid.map Submonoid.LocalizationMap CommMonoidWithZero.toCommMonoid instFunLike instMonoidHomClass nonZeroDivisors	—	instMonoidHomClass Submonoid.map_le_iff_le_comap nonZeroDivisors_le_comap
map_zero 📖	mathematical	—	DFunLike.coe Submonoid.LocalizationMap CommMonoidWithZero.toCommMonoid instFunLike MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	surj MulZeroClass.zero_mul map_mul MonoidHomClass.toMulHomClass instMonoidHomClass MulZeroClass.mul_zero
mk'_eq_zero_iff 📖	mathematical	—	mk' CommMonoidWithZero.toCommMonoid MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MulZeroClass.toMul Submonoid MulZeroOneClass.toMulOneClass SetLike.instMembership Submonoid.instSetLike	—	map_units mk'_spec MulZeroClass.zero_mul map_eq_zero_iff
mk'_zero 📖	mathematical	—	mk' CommMonoidWithZero.toCommMonoid MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	eq_mk'_iff_mul_eq MulZeroClass.zero_mul map_zero
noZeroDivisors 📖	mathematical	—	NoZeroDivisors MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MulZeroClass.toZero	—	noZeroDivisors_iff_forall_mem_nonZeroDivisors surj IsUnit.mul_left_eq_zero map_units map_zero mul_mem_nonZeroDivisors map_nonZeroDivisors_le mem_nonZeroDivisors_of_ne_zero
nonZeroDivisors_le_comap 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Submonoid.comap Submonoid.LocalizationMap CommMonoidWithZero.toCommMonoid instFunLike instMonoidHomClass	—	instMonoidHomClass surj IsUnit.mul_left_eq_zero map_units map_eq_zero_iff mul_right_mem_nonZeroDivisorsRight_eq_zero_iff map_mul MonoidHomClass.toMulHomClass mul_right_comm nonZeroDivisorsRight_eq_nonZeroDivisors
nontrivial 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	Nontrivial	—	not_subsingleton_iff_nontrivial subsingleton_iff
sec_zero_fst 📖	mathematical	—	DFunLike.coe Submonoid.LocalizationMap CommMonoidWithZero.toCommMonoid instFunLike Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike sec MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	sec_spec' MulZeroClass.mul_zero
subsingleton 📖	—	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	—	—	mk'_sec eq MulZeroClass.zero_mul
subsingleton_iff 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	—	exists_of_eq mul_one MulZeroClass.mul_zero subsingleton

(root)

Definitions

Name	Category	Theorems
MonoidWithZero 📖	CompData	—

---

← Back to Index