Basic

📁 Source: Mathlib/Algebra/GroupWithZero/Pointwise/Set/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems div_zero, mul_zero, zero_div, zero_mul, div_zero_subset, inv_zero, mul_zero_subset, zero_div_subset, zero_mul_subset	9
Total	9

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
div_zero_subset 📖	mathematical	—	Set instHasSubset div DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid zero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	—	div_zero
inv_zero 📖	mathematical	—	Set inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid zero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	—	ext
mul_zero_subset 📖	mathematical	—	Set instHasSubset mul MulZeroClass.toMul zero MulZeroClass.toZero	—	MulZeroClass.mul_zero
zero_div_subset 📖	mathematical	—	Set instHasSubset div DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid zero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	—	zero_div
zero_mul_subset 📖	mathematical	—	Set instHasSubset mul MulZeroClass.toMul zero MulZeroClass.toZero	—	MulZeroClass.zero_mul

Set.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
div_zero 📖	mathematical	Set.Nonempty	Set Set.div DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid Set.zero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	—	HasSubset.Subset.antisymm Set.instAntisymmSubset Set.div_zero_subset div_zero
mul_zero 📖	mathematical	Set.Nonempty	Set Set.mul MulZeroClass.toMul Set.zero MulZeroClass.toZero	—	HasSubset.Subset.antisymm Set.instAntisymmSubset Set.mul_zero_subset MulZeroClass.mul_zero
zero_div 📖	mathematical	Set.Nonempty	Set Set.div DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid Set.zero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	—	HasSubset.Subset.antisymm Set.instAntisymmSubset Set.zero_div_subset zero_div
zero_mul 📖	mathematical	Set.Nonempty	Set Set.mul MulZeroClass.toMul Set.zero MulZeroClass.toZero	—	HasSubset.Subset.antisymm Set.instAntisymmSubset Set.zero_mul_subset MulZeroClass.zero_mul

---

← Back to Index