Documentation Verification Report

Finset

📁 Source: Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean

Statistics

Metric	Count
Definitions	0
Theorems `div_zero`, `mul_zero`, `zero_div`, `zero_mul`, `card_le_card_mul_left₀`, `card_le_card_mul_right₀`, `card_le_card_mul_self₀`, `div_zero_subset`, `inv_zero`, `mul_zero_subset`, `zero_div_subset`, `zero_mul_subset`	12
Total	12

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_card_mul_left₀` 📖	mathematical	`Finset` `instMembership`	`card` `mul`	—	`card_le_card_mul_left_of_injective` `mul_right_injective₀`
`card_le_card_mul_right₀` 📖	mathematical	`Finset` `instMembership`	`card` `mul`	—	`card_le_card_mul_right_of_injective` `mul_left_injective₀`
`card_le_card_mul_self₀` 📖	mathematical	—	`card` `Finset` `mul`	—	`eq_empty_or_nonempty` `erase_eq_empty_iff` `mul_empty` `card_singleton` `singleton_mul_singleton` `card_le_card_mul_left₀`
`div_zero_subset` 📖	mathematical	—	`Finset` `instHasSubset` `div` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `zero` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	—	`div_zero`
`inv_zero` 📖	mathematical	—	`Finset` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `zero` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	—	`ext`
`mul_zero_subset` 📖	mathematical	—	`Finset` `instHasSubset` `mul` `MulZeroClass.toMul` `zero` `MulZeroClass.toZero`	—	`MulZeroClass.mul_zero`
`zero_div_subset` 📖	mathematical	—	`Finset` `instHasSubset` `div` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `zero` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	—	`zero_div`
`zero_mul_subset` 📖	mathematical	—	`Finset` `instHasSubset` `mul` `MulZeroClass.toMul` `zero` `MulZeroClass.toZero`	—	`MulZeroClass.zero_mul`

Finset.Nonempty

Theorems

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

---

← Back to Index