Documentation Verification Report

Dissociation

📁 Source: Mathlib/Combinatorics/Additive/Dissociation.lean

Statistics

Metric	Count
Definitions `AddDissociated`, `addSpan`, `mulSpan`, `MulDissociated`	4
Theorems `neg`, `of_neg`, `subset`, `addDissociated_preimage`, `exists_subset_addSpan_card_le_of_forall_addDissociated`, `exists_subset_mulSpan_card_le_of_forall_mulDissociated`, `mem_addSpan`, `mem_mulSpan`, `prod_div_prod_mem_mulSpan`, `subset_addSpan`, `subset_mulSpan`, `sum_sub_sum_mem_addSpan`, `inv`, `of_inv`, `subset`, `mulDissociated_preimage`, `addDissociated_empty`, `addDissociated_iff_sum_eq_subsingleton`, `addDissociated_neg`, `addDissociated_singleton`, `mulDissociated_empty`, `mulDissociated_iff_sum_eq_subsingleton`, `mulDissociated_inv`, `mulDissociated_singleton`, `not_addDissociated`, `not_addDissociated_iff_exists_disjoint`, `not_mulDissociated`, `not_mulDissociated_iff_exists_disjoint`	28
Total	32

AddDissociated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`neg` 📖	mathematical	`AddDissociated`	`Set` `InvolutiveNeg.toNeg` `Set.involutiveNeg` `SubtractionMonoid.toInvolutiveNeg` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`addDissociated_neg`
`of_neg` 📖	—	`AddDissociated` `Set` `InvolutiveNeg.toNeg` `Set.involutiveNeg` `SubtractionMonoid.toInvolutiveNeg` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—	`addDissociated_neg`
`subset` 📖	—	`Set` `Set.instHasSubset` `AddDissociated`	—	—	`Set.InjOn.mono` `LE.le.trans'`

AddEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addDissociated_preimage` 📖	mathematical	—	`AddDissociated` `Set.preimage` `DFunLike.coe` `AddEquiv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `EquivLike.toFunLike` `instEquivLike`	—	`apply_eq_iff_eq` `map_sum` `AddEquivClass.instAddMonoidHomClass` `instAddEquivClass` `Equiv.forall_congr_right` `Finset.coe_map` `Set.image_congr` `Set.image_subset_iff` `Finset.sum_map` `Finset.sum_congr` `Finset.map_injective`

Finset

Definitions

Name	Category	Theorems
`addSpan` 📖	CompOp	4 math math: `subset_addSpan`, `sum_sub_sum_mem_addSpan`, `mem_addSpan`, `exists_subset_addSpan_card_le_of_forall_addDissociated`
`mulSpan` 📖	CompOp	4 math math: `mem_mulSpan`, `prod_div_prod_mem_mulSpan`, `subset_mulSpan`, `exists_subset_mulSpan_card_le_of_forall_mulDissociated`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_subset_addSpan_card_le_of_forall_addDissociated` 📖	mathematical	`card`	`Finset` `instHasSubset` `addSpan`	—	`exists_maximal` `instIsTransLe` `mem_filter` `empty_mem_powerset` `coe_empty` `addDissociated_empty` `mem_powerset` `subset_addSpan` `not_addDissociated_iff_exists_disjoint` `Maximal.not_gt` `insert_subset_iff` `ssubset_insert` `sum_erase_eq_sub` `sub_sub_self` `sum_sub_sum_mem_addSpan` `subset_insert_iff_of_notMem` `disjoint_left` `subset_insert_iff` `coe_subset`
`exists_subset_mulSpan_card_le_of_forall_mulDissociated` 📖	mathematical	`card`	`Finset` `instHasSubset` `mulSpan`	—	`exists_maximal` `instIsTransLe` `mem_filter` `empty_mem_powerset` `coe_empty` `subset_mulSpan` `not_mulDissociated_iff_exists_disjoint` `Maximal.not_gt` `insert_subset_iff` `ssubset_insert` `prod_erase_eq_div` `div_div_self'` `prod_div_prod_mem_mulSpan` `subset_insert_iff_of_notMem` `disjoint_left` `subset_insert_iff` `coe_subset`
`mem_addSpan` 📖	mathematical	—	`Finset` `instMembership` `addSpan` `sum` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`mem_image` `Fintype.mem_piFinset` `mem_insert` `mem_singleton`
`mem_mulSpan` 📖	mathematical	—	`Finset` `instMembership` `mulSpan` `prod` `CommGroup.toCommMonoid` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	—
`prod_div_prod_mem_mulSpan` 📖	mathematical	`Finset` `instHasSubset`	`instMembership` `mulSpan` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `prod` `CommGroup.toCommMonoid`	—	`mem_mulSpan` `Set.indicator_of_mem` `sub_self` `Set.indicator_of_notMem` `sub_zero` `zero_sub` `prod_congr` `zpow_sub` `pow_ite` `zpow_one` `zpow_zero` `prod_div_distrib` `prod_ite_mem` `inter_eq_right`
`subset_addSpan` 📖	mathematical	—	`Finset` `instHasSubset` `addSpan`	—	`mem_addSpan` `eq_or_ne` `Pi.single_eq_same` `one_ne_zero` `Pi.single_eq_of_ne'` `zero_eq_neg` `zero_ne_one` `sum_congr` `ite_smul` `one_zsmul` `zero_zsmul` `sum_ite_eq'`
`subset_mulSpan` 📖	mathematical	—	`Finset` `instHasSubset` `mulSpan`	—	`mem_mulSpan` `eq_or_ne` `Pi.single_eq_same` `Pi.single_eq_of_ne'` `prod_congr` `pow_ite` `zpow_one` `zpow_zero` `prod_ite_eq'`
`sum_sub_sum_mem_addSpan` 📖	mathematical	`Finset` `instHasSubset`	`instMembership` `addSpan` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `sum` `AddCommGroup.toAddCommMonoid`	—	`mem_addSpan` `Set.indicator_of_mem` `SetLike.mem_coe` `sub_self` `zero_eq_neg` `one_ne_zero` `zero_ne_one` `Set.indicator_of_notMem` `sub_zero` `zero_sub` `neg_eq_zero` `sum_congr` `sub_zsmul` `ite_smul` `one_zsmul` `zero_zsmul` `sub_eq_add_neg` `sum_sub_distrib` `sum_ite_mem` `inter_eq_right`

MulDissociated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv` 📖	mathematical	`MulDissociated`	`Set` `InvolutiveInv.toInv` `Set.involutiveInv` `DivisionMonoid.toInvolutiveInv` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	`mulDissociated_inv`
`of_inv` 📖	—	`MulDissociated` `Set` `InvolutiveInv.toInv` `Set.involutiveInv` `DivisionMonoid.toInvolutiveInv` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	—	`mulDissociated_inv`
`subset` 📖	—	`Set` `Set.instHasSubset` `MulDissociated`	—	—	`Set.InjOn.mono` `LE.le.trans'`

MulEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulDissociated_preimage` 📖	mathematical	—	`MulDissociated` `Set.preimage` `DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `EquivLike.toFunLike` `instEquivLike`	—	`apply_eq_iff_eq` `map_prod` `MulEquivClass.instMonoidHomClass` `instMulEquivClass` `Equiv.forall_congr_right` `Finset.coe_map` `Set.image_congr` `Finset.prod_map` `Finset.prod_congr` `Finset.map_injective`

(root)

Definitions

Name	Category	Theorems
`AddDissociated` 📖	MathDef	7 math math: `not_addDissociated`, `addDissociated_neg`, `not_addDissociated_iff_exists_disjoint`, `AddEquiv.addDissociated_preimage`, `addDissociated_singleton`, `addDissociated_iff_sum_eq_subsingleton`, `addDissociated_empty`
`MulDissociated` 📖	MathDef	7 math math: `mulDissociated_inv`, `not_mulDissociated`, `mulDissociated_empty`, `not_mulDissociated_iff_exists_disjoint`, `MulEquiv.mulDissociated_preimage`, `mulDissociated_singleton`, `mulDissociated_iff_sum_eq_subsingleton`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addDissociated_empty` 📖	mathematical	—	`AddDissociated` `Set` `Set.instEmptyCollection`	—	`Set.subset_empty_iff` `Finset.coe_eq_empty` `Set.injOn_singleton`
`addDissociated_iff_sum_eq_subsingleton` 📖	mathematical	—	`AddDissociated` `Set.Subsingleton` `Finset` `setOf` `Set` `Set.instHasSubset` `SetLike.coe` `Finset.instSetLike` `Finset.sum` `AddCommGroup.toAddCommMonoid`	—	—
`addDissociated_neg` 📖	mathematical	—	`AddDissociated` `Set` `InvolutiveNeg.toNeg` `Set.involutiveNeg` `SubtractionMonoid.toInvolutiveNeg` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`AddEquiv.addDissociated_preimage`
`addDissociated_singleton` 📖	mathematical	—	`AddDissociated` `Set` `Set.instSingletonSet`	—	`Finset.coe_subset_singleton` `Finset.subset_singleton_iff` `Set.union_singleton` `Set.injOn_pair` `Finset.sum_singleton` `Finset.singleton_ne_empty`
`mulDissociated_empty` 📖	mathematical	—	`MulDissociated` `Set` `Set.instEmptyCollection`	—	—
`mulDissociated_iff_sum_eq_subsingleton` 📖	mathematical	—	`MulDissociated` `Set.Subsingleton` `Finset` `setOf` `Set` `Set.instHasSubset` `SetLike.coe` `Finset.instSetLike` `Finset.prod` `CommGroup.toCommMonoid`	—	—
`mulDissociated_inv` 📖	mathematical	—	`MulDissociated` `Set` `InvolutiveInv.toInv` `Set.involutiveInv` `DivisionMonoid.toInvolutiveInv` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	`MulEquiv.mulDissociated_preimage`
`mulDissociated_singleton` 📖	mathematical	—	`MulDissociated` `Set` `Set.instSingletonSet`	—	`Set.union_singleton` `Finset.prod_singleton`
`not_addDissociated` 📖	mathematical	—	`AddDissociated` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.sum` `AddCommGroup.toAddCommMonoid`	—	—
`not_addDissociated_iff_exists_disjoint` 📖	mathematical	—	`AddDissociated` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Disjoint` `Finset.partialOrder` `Finset.instOrderBot` `Finset.sum` `AddCommGroup.toAddCommMonoid`	—	`not_addDissociated` `Finset.coe_sdiff` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.diff_subset` `disjoint_sdiff_sdiff` `sdiff_ne_sdiff_iff` `Finset.sum_sdiff_eq_sum_sdiff_iff`
`not_mulDissociated` 📖	mathematical	—	`MulDissociated` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.prod` `CommGroup.toCommMonoid`	—	—
`not_mulDissociated_iff_exists_disjoint` 📖	mathematical	—	`MulDissociated` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Disjoint` `Finset.partialOrder` `Finset.instOrderBot` `Finset.prod` `CommGroup.toCommMonoid`	—	`not_mulDissociated` `Finset.coe_sdiff` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.diff_subset` `disjoint_sdiff_sdiff` `sdiff_ne_sdiff_iff` `Finset.prod_sdiff_eq_prod_sdiff_iff`

---

← Back to Index