Documentation Verification Report

Basic

📁 Source: Mathlib/Algebra/Group/UniqueProds/Basic.lean

Statistics

Metric	Count
Definitions `TwoUniqueProds`, `TwoUniqueSums`, `UniqueAdd`, `UniqueMul`	4
Theorems `twoUniqueSums_iff`, `uniqueSums_iff`, `instTwoUniqueSumsOfTwoUniqueProds`, `instUniqueSumsOfUniqueProds`, `twoUniqueProds_iff`, `uniqueProds_iff`, `instTwoUniqueProdsOfTwoUniqueSums`, `instUniqueProdsOfUniqueSums`, `instTwoUniqueProds`, `instTwoUniqueSums`, `instUniqueProds`, `instUniqueSums`, `instForall`, `instMulOpposite`, `of_covariant_left`, `of_covariant_right`, `of_injective_mulHom`, `of_mulHom`, `of_mulOpposite`, `toUniqueProds`, `uniqueMul_of_one_lt_card`, `instAddOpposite`, `instForall`, `of_addHom`, `of_addOpposite`, `of_covariant_left`, `of_covariant_right`, `of_injective_addHom`, `toUniqueSums`, `uniqueAdd_of_one_lt_card`, `addHom_image_iff`, `addHom_map_iff`, `addHom_preimage`, `exists_iff_exists_existsUnique`, `iff_addOpposite`, `iff_card_le_one`, `iff_existsUnique`, `mono`, `mt`, `of_addHom_image`, `of_addOpposite`, `of_card_le_one`, `of_image_filter`, `of_subsingleton`, `set_subsingleton`, `subsingleton`, `to_addOpposite`, `exists_iff_exists_existsUnique`, `iff_card_le_one`, `iff_existsUnique`, `iff_mulOpposite`, `mono`, `mt`, `mulHom_image_iff`, `mulHom_map_iff`, `mulHom_preimage`, `of_card_le_one`, `of_image_filter`, `of_mulHom_image`, `of_mulOpposite`, `of_subsingleton`, `set_subsingleton`, `subsingleton`, `to_mulOpposite`, `instForall`, `instMulOpposite`, `of_injective_mulHom`, `of_mulHom`, `of_mulOpposite`, `of_same`, `toIsCancelMul`, `toTwoUniqueProds_of_group`, `uniqueMul_of_nonempty`, `instAddOpposite`, `instForall`, `of_addHom`, `of_addOpposite`, `of_injective_addHom`, `of_same`, `toIsCancelAdd`, `toTwoUniqueSums_of_addGroup`, `uniqueAdd_of_nonempty`, `instTwoUniqueSumsDFinsupp`, `instTwoUniqueSumsFinsupp`, `instUniqueSumsDFinsupp`, `instUniqueSumsFinsupp`, `uniqueAdd_of_twoUniqueAdd`, `uniqueMul_of_twoUniqueMul`	88
Total	92

AddEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`twoUniqueSums_iff` 📖	mathematical	—	`TwoUniqueSums`	—	`TwoUniqueSums.of_injective_addHom` `AddEquivClass.instAddHomClass` `instAddEquivClass` `injective`
`uniqueSums_iff` 📖	mathematical	—	`UniqueSums`	—	`UniqueSums.of_injective_addHom` `AddEquivClass.instAddHomClass` `instAddEquivClass` `injective`

Additive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instTwoUniqueSumsOfTwoUniqueProds` 📖	mathematical	—	`TwoUniqueSums` `Additive` `add`	—	`TwoUniqueProds.uniqueMul_of_one_lt_card`
`instUniqueSumsOfUniqueProds` 📖	mathematical	—	`UniqueSums` `Additive` `add`	—	`UniqueProds.uniqueMul_of_nonempty`

MulEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`twoUniqueProds_iff` 📖	mathematical	—	`TwoUniqueProds`	—	`TwoUniqueProds.of_injective_mulHom` `MulEquivClass.instMulHomClass` `instMulEquivClass` `injective`
`uniqueProds_iff` 📖	mathematical	—	`UniqueProds`	—	`UniqueProds.of_injective_mulHom` `MulEquivClass.instMulHomClass` `instMulEquivClass` `injective`

Multiplicative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instTwoUniqueProdsOfTwoUniqueSums` 📖	mathematical	—	`TwoUniqueProds` `Multiplicative` `mul`	—	`TwoUniqueSums.uniqueAdd_of_one_lt_card`
`instUniqueProdsOfUniqueSums` 📖	mathematical	—	`UniqueProds` `Multiplicative` `mul`	—	`UniqueSums.uniqueAdd_of_nonempty`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instTwoUniqueProds` 📖	mathematical	—	`TwoUniqueProds` `instMul`	—	`TwoUniqueProds.of_injective_mulHom` `ULift.down_injective` `ULift.up_injective` `TwoUniqueProds.instForall`
`instTwoUniqueSums` 📖	mathematical	—	`TwoUniqueSums` `instAdd`	—	`TwoUniqueSums.of_injective_addHom` `ULift.down_injective` `ULift.up_injective` `TwoUniqueSums.instForall`
`instUniqueProds` 📖	mathematical	—	`UniqueProds` `instMul`	—	`UniqueProds.of_injective_mulHom` `ULift.down_injective` `ULift.up_injective` `UniqueProds.instForall`
`instUniqueSums` 📖	mathematical	—	`UniqueSums` `instAdd`	—	`UniqueSums.of_injective_addHom` `ULift.down_injective` `ULift.up_injective` `UniqueSums.instForall`

TwoUniqueProds

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instForall` 📖	mathematical	`TwoUniqueProds`	`Pi.instMul`	—	`Finset.isWellFounded_ssubset` `IsWellFounded.induction` `Finset.exists_of_one_lt_card_pi` `uniqueMul_of_one_lt_card` `Finset.card_pos` `Finset.Nonempty.image` `uniqueMul_of_twoUniqueMul` `HasSubset.Subset.ssubset_of_ne` `Finset.instIsNonstrictStrictOrderSubsetSSubset` `Finset.instAntisymmSubset` `Finset.filter_subset` `Finset.mem_filter` `UniqueMul.of_image_filter`
`instMulOpposite` 📖	mathematical	—	`TwoUniqueProds` `MulOpposite` `MulOpposite.instMul`	—	`of_mulOpposite` `MulEquiv.twoUniqueProds_iff`
`of_covariant_left` 📖	mathematical	—	`TwoUniqueProds`	—	`MulOpposite.unop_injective` `mul_lt_mul_left` `of_mulOpposite` `of_covariant_right` `MulOpposite.instIsRightCancelMul`
`of_covariant_right` 📖	mathematical	—	`TwoUniqueProds`	—	`Finset.Nonempty.mul` `Finset.card_pos` `Finset.mem_mul` `Finset.max'_mem` `Finset.min'_mem` `lt_trichotomy` `LT.lt.not_ge` `mul_lt_mul_right` `Finset.le_max'` `Finset.mul_mem_mul` `mul_right_cancel` `Finset.mk_mem_product` `Finset.exists_mem_ne` `Finset.card_product` `LT.lt.ne` `Finset.min'_lt_max'` `Finset.mem_product` `Finset.min'_le`
`of_injective_mulHom` 📖	mathematical	`DFunLike.coe` `MulHom` `MulHom.funLike`	`TwoUniqueProds`	—	`of_mulHom`
`of_mulHom` 📖	mathematical	—	`TwoUniqueProds`	—	`lt_or_ge` `uniqueMul_of_one_lt_card` `UniqueMul.of_mulHom_image` `Finset.one_lt_card_iff_nontrivial` `Finset.card_product` `Finset.mem_product` `UniqueMul.iff_card_le_one` `Finset.mem_image_of_mem` `LE.le.trans` `Finset.card_filter_le`
`of_mulOpposite` 📖	mathematical	—	`TwoUniqueProds`	—	`MulOpposite.op_injective` `uniqueMul_of_one_lt_card` `mul_comm` `Finset.card_map` `Finset.mem_map'` `Mathlib.Tactic.Contrapose.contrapose₄` `MulOpposite.unop_injective` `UniqueMul.of_mulOpposite`
`toUniqueProds` 📖	mathematical	—	`UniqueProds`	—	`uniqueMul_of_twoUniqueMul` `uniqueMul_of_one_lt_card`
`uniqueMul_of_one_lt_card` 📖	mathematical	`Finset.card`	`Finset` `Finset.instMembership` `SProd.sprod` `Finset.instSProd` `UniqueMul`	—	—

TwoUniqueSums

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAddOpposite` 📖	mathematical	—	`TwoUniqueSums` `AddOpposite` `AddOpposite.instAdd`	—	`of_addOpposite` `AddEquiv.twoUniqueSums_iff`
`instForall` 📖	mathematical	`TwoUniqueSums`	`Pi.instAdd`	—	`Finset.isWellFounded_ssubset` `IsWellFounded.induction` `Finset.exists_of_one_lt_card_pi` `uniqueAdd_of_one_lt_card` `Finset.card_pos` `Finset.Nonempty.image` `uniqueAdd_of_twoUniqueAdd` `HasSubset.Subset.ssubset_of_ne` `Finset.instIsNonstrictStrictOrderSubsetSSubset` `Finset.instAntisymmSubset` `Finset.filter_subset` `Finset.filter_nonempty_iff` `Finset.mem_image` `Finset.mem_product` `Finset.mem_filter` `UniqueAdd.of_image_filter`
`of_addHom` 📖	mathematical	—	`TwoUniqueSums`	—	`lt_or_ge` `uniqueAdd_of_one_lt_card` `Finset.mem_product` `Finset.mem_image` `UniqueAdd.of_addHom_image` `Finset.one_lt_card_iff_nontrivial` `Finset.card_product` `UniqueAdd.iff_card_le_one` `Finset.mem_image_of_mem` `LE.le.trans` `Finset.card_filter_le`
`of_addOpposite` 📖	mathematical	—	`TwoUniqueSums`	—	`AddOpposite.op_injective` `uniqueAdd_of_one_lt_card` `mul_comm` `Finset.card_map` `Finset.mem_product` `Finset.mem_map'` `Mathlib.Tactic.Contrapose.contrapose₄` `AddOpposite.unop_injective` `UniqueAdd.of_addOpposite`
`of_covariant_left` 📖	mathematical	—	`TwoUniqueSums`	—	`AddOpposite.unop_injective` `add_lt_add_left` `of_addOpposite` `of_covariant_right` `AddOpposite.instIsRightCancelAdd`
`of_covariant_right` 📖	mathematical	—	`TwoUniqueSums`	—	`Finset.Nonempty.add` `Finset.card_pos` `Finset.mem_add` `Finset.max'_mem` `Finset.min'_mem` `lt_trichotomy` `LT.lt.not_ge` `add_lt_add_right` `Finset.le_max'` `Finset.add_mem_add` `add_right_cancel` `Finset.mk_mem_product` `Finset.exists_mem_ne` `Finset.card_product` `LT.lt.ne` `Finset.min'_lt_max'` `Finset.mem_product` `Finset.min'_le`
`of_injective_addHom` 📖	mathematical	`DFunLike.coe` `AddHom` `AddHom.funLike`	`TwoUniqueSums`	—	`of_addHom`
`toUniqueSums` 📖	mathematical	—	`UniqueSums`	—	`uniqueAdd_of_twoUniqueAdd` `uniqueAdd_of_one_lt_card`
`uniqueAdd_of_one_lt_card` 📖	mathematical	`Finset.card`	`Finset` `Finset.instMembership` `SProd.sprod` `Finset.instSProd` `UniqueAdd`	—	—

UniqueAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addHom_image_iff` 📖	mathematical	`DFunLike.coe` `AddHom` `AddHom.funLike`	`UniqueAdd` `Finset.image`	—	`of_addHom_image` `Finset.mem_image` `map_add` `AddHom.addHomClass`
`addHom_map_iff` 📖	mathematical	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	`UniqueAdd` `Finset.map`	—	`addHom_image_iff` `Function.Embedding.inj'` `Finset.map_eq_image`
`addHom_preimage` 📖	mathematical	`DFunLike.coe` `AddHom` `AddHom.funLike` `UniqueAdd`	`Finset.preimage` `Function.Injective.injOn` `Set.preimage` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Function.Injective.injOn` `Finset.mem_preimage` `map_add` `AddHom.addHomClass`
`exists_iff_exists_existsUnique` 📖	mathematical	—	`Finset` `Finset.instMembership` `UniqueAdd` `ExistsUnique` `SProd.sprod` `Finset.instSProd`	—	`iff_existsUnique` `Finset.mem_product`
`iff_addOpposite` 📖	mathematical	—	`UniqueAdd` `AddOpposite` `AddOpposite.instAdd` `Finset.map` `AddOpposite.op` `AddOpposite.op_injective`	—	`AddOpposite.op_injective` `of_addOpposite` `to_addOpposite`
`iff_card_le_one` 📖	mathematical	`Finset` `Finset.instMembership`	`UniqueAdd` `Finset.card` `Finset.filter` `SProd.sprod` `Finset.instSProd`	—	`Finset.card_le_one_iff` `Finset.mem_filter` `Finset.mem_product`
`iff_existsUnique` 📖	mathematical	`Finset` `Finset.instMembership`	`UniqueAdd` `ExistsUnique` `SProd.sprod` `Finset.instSProd`	—	`Finset.mk_mem_product` `Finset.mem_product` `ExistsUnique.elim`
`mono` 📖	—	`Finset` `Finset.instHasSubset` `UniqueAdd`	—	—	—
`mt` 📖	—	`UniqueAdd` `Finset` `Finset.instMembership`	—	—	`Mathlib.Tactic.Contrapose.contrapose₃`
`of_addHom_image` 📖	—	`UniqueAdd` `Finset.image` `DFunLike.coe` `AddHom` `AddHom.funLike`	—	—	`Finset.mem_image_of_mem` `map_add` `AddHom.addHomClass`
`of_addOpposite` 📖	—	`UniqueAdd` `AddOpposite` `AddOpposite.instAdd` `Finset.map` `AddOpposite.op` `AddOpposite.op_injective`	—	—	`AddOpposite.op_injective` `Finset.mem_map_of_mem`
`of_card_le_one` 📖	mathematical	`Finset.Nonempty` `Finset.card`	`Finset` `Finset.instMembership` `UniqueAdd`	—	`Finset.card_le_one_iff`
`of_image_filter` 📖	—	`DFunLike.coe` `AddHom` `AddHom.funLike` `UniqueAdd` `Finset.image` `Finset.filter`	—	—	`Finset.mem_filter` `map_add` `AddHom.addHomClass` `Finset.mem_image_of_mem`
`of_subsingleton` 📖	mathematical	—	`UniqueAdd`	—	—
`set_subsingleton` 📖	mathematical	`UniqueAdd`	`Set.Subsingleton` `setOf` `Finset` `Finset.instMembership`	—	—
`subsingleton` 📖	mathematical	`UniqueAdd`	`Finset` `Finset.instMembership`	—	—
`to_addOpposite` 📖	mathematical	`UniqueAdd`	`AddOpposite` `AddOpposite.instAdd` `Finset.map` `AddOpposite.op` `AddOpposite.op_injective`	—	`of_addOpposite` `AddOpposite.op_injective` `Finset.map_map` `addHom_map_iff`

UniqueMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_iff_exists_existsUnique` 📖	mathematical	—	`Finset` `Finset.instMembership` `UniqueMul` `ExistsUnique` `SProd.sprod` `Finset.instSProd`	—	`iff_existsUnique` `Finset.mem_product`
`iff_card_le_one` 📖	mathematical	`Finset` `Finset.instMembership`	`UniqueMul` `Finset.card` `Finset.filter` `SProd.sprod` `Finset.instSProd`	—	—
`iff_existsUnique` 📖	mathematical	`Finset` `Finset.instMembership`	`UniqueMul` `ExistsUnique` `SProd.sprod` `Finset.instSProd`	—	`Finset.mk_mem_product` `ExistsUnique.elim`
`iff_mulOpposite` 📖	mathematical	—	`UniqueMul` `MulOpposite` `MulOpposite.instMul` `Finset.map` `MulOpposite.op` `MulOpposite.op_injective`	—	`MulOpposite.op_injective` `of_mulOpposite` `to_mulOpposite`
`mono` 📖	—	`Finset` `Finset.instHasSubset` `UniqueMul`	—	—	—
`mt` 📖	—	`UniqueMul` `Finset` `Finset.instMembership`	—	—	`Mathlib.Tactic.Contrapose.contrapose₃`
`mulHom_image_iff` 📖	mathematical	`DFunLike.coe` `MulHom` `MulHom.funLike`	`UniqueMul` `Finset.image`	—	`of_mulHom_image` `MulHom.mulHomClass`
`mulHom_map_iff` 📖	mathematical	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	`UniqueMul` `Finset.map`	—	`mulHom_image_iff` `Function.Embedding.inj'` `Finset.map_eq_image`
`mulHom_preimage` 📖	mathematical	`DFunLike.coe` `MulHom` `MulHom.funLike` `UniqueMul`	`Finset.preimage` `Function.Injective.injOn` `Set.preimage` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Function.Injective.injOn` `Finset.mem_preimage` `map_mul` `MulHom.mulHomClass`
`of_card_le_one` 📖	mathematical	`Finset.Nonempty` `Finset.card`	`Finset` `Finset.instMembership` `UniqueMul`	—	`Finset.card_le_one_iff`
`of_image_filter` 📖	—	`DFunLike.coe` `MulHom` `MulHom.funLike` `UniqueMul` `Finset.image` `Finset.filter`	—	—	`Finset.mem_filter` `map_mul` `MulHom.mulHomClass` `Finset.mem_image_of_mem`
`of_mulHom_image` 📖	—	`UniqueMul` `Finset.image` `DFunLike.coe` `MulHom` `MulHom.funLike`	—	—	`Finset.mem_image_of_mem` `MulHom.mulHomClass`
`of_mulOpposite` 📖	—	`UniqueMul` `MulOpposite` `MulOpposite.instMul` `Finset.map` `MulOpposite.op` `MulOpposite.op_injective`	—	—	`MulOpposite.op_injective` `Finset.mem_map_of_mem`
`of_subsingleton` 📖	mathematical	—	`UniqueMul`	—	—
`set_subsingleton` 📖	mathematical	`UniqueMul`	`Set.Subsingleton` `setOf` `Finset` `Finset.instMembership`	—	—
`subsingleton` 📖	mathematical	`UniqueMul`	`Finset` `Finset.instMembership`	—	—
`to_mulOpposite` 📖	mathematical	`UniqueMul`	`MulOpposite` `MulOpposite.instMul` `Finset.map` `MulOpposite.op` `MulOpposite.op_injective`	—	`of_mulOpposite` `MulOpposite.op_injective` `Finset.map_map` `mulHom_map_iff`

UniqueProds

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instForall` 📖	mathematical	`UniqueProds`	`Pi.instMul`	—	`Finset.isWellFounded_ssubset` `IsWellFounded.induction` `UniqueMul.of_card_le_one` `Finset.exists_of_one_lt_card_pi` `Mathlib.Tactic.Push.not_and_or_eq` `uniqueMul_of_nonempty` `Finset.Nonempty.image` `Finset.filter_nonempty_iff` `Finset.mem_image` `HasSubset.Subset.ssubset_of_ne` `Finset.instIsNonstrictStrictOrderSubsetSSubset` `Finset.instAntisymmSubset` `Finset.filter_subset` `Finset.mem_filter` `UniqueMul.of_image_filter`
`instMulOpposite` 📖	mathematical	—	`UniqueProds` `MulOpposite` `MulOpposite.instMul`	—	`of_mulOpposite` `MulEquiv.uniqueProds_iff`
`of_injective_mulHom` 📖	mathematical	`DFunLike.coe` `MulHom` `MulHom.funLike`	`UniqueProds`	—	`of_mulHom`
`of_mulHom` 📖	mathematical	—	`UniqueProds`	—	`uniqueMul_of_nonempty` `Finset.Nonempty.image` `Finset.mem_image` `UniqueMul.of_mulHom_image`
`of_mulOpposite` 📖	mathematical	—	`UniqueProds`	—	`MulOpposite.op_injective` `uniqueMul_of_nonempty` `Finset.Nonempty.map` `Finset.mem_map'` `UniqueMul.of_mulOpposite`
`of_same` 📖	mathematical	`Finset` `Finset.instMembership` `UniqueMul` `Semigroup.toMul`	`UniqueProds`	—	`Finset.Nonempty.mul` `Finset.mem_mul` `mul_left_cancel` `IsCancelMul.toIsLeftCancelMul` `Finset.mul_mem_mul` `mul_assoc` `mul_right_cancel` `IsCancelMul.toIsRightCancelMul`
`toIsCancelMul` 📖	mathematical	—	`IsCancelMul`	—	`MulOpposite.op_injective` `IsLeftCancelMul.mul_left_cancel` `instMulOpposite` `MulOpposite.unop_injective`
`toTwoUniqueProds_of_group` 📖	mathematical	—	`TwoUniqueProds` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`uniqueMul_of_nonempty` `mul_right_injective` `LeftCancelSemigroup.toIsLeftCancelMul` `mul_left_injective` `RightCancelSemigroup.toIsRightCancelMul` `Finset.card_map` `Finset.mem_map` `inv_mul_cancel` `mul_inv_cancel` `Finset.Nonempty.mul` `Finset.Nonempty.image` `Finset.Nonempty.map` `mul_assoc` `mul_right_cancel_iff` `mul_left_cancel_iff` `mul_one` `one_mul` `Finset.exists_mem_ne` `inv_one` `not_and_or` `Finset.mem_map_of_mem`
`uniqueMul_of_nonempty` 📖	mathematical	`Finset.Nonempty`	`Finset` `Finset.instMembership` `UniqueMul`	—	—

UniqueSums

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAddOpposite` 📖	mathematical	—	`UniqueSums` `AddOpposite` `AddOpposite.instAdd`	—	`of_addOpposite` `AddEquiv.uniqueSums_iff`
`instForall` 📖	mathematical	`UniqueSums`	`Pi.instAdd`	—	`Finset.isWellFounded_ssubset` `IsWellFounded.induction` `UniqueAdd.of_card_le_one` `Finset.exists_of_one_lt_card_pi` `Mathlib.Tactic.Push.not_and_or_eq` `not_le` `uniqueAdd_of_nonempty` `Finset.Nonempty.image` `Finset.filter_nonempty_iff` `Finset.mem_image` `HasSubset.Subset.ssubset_of_ne` `Finset.instIsNonstrictStrictOrderSubsetSSubset` `Finset.instAntisymmSubset` `Finset.filter_subset` `Finset.mem_filter` `UniqueAdd.of_image_filter`
`of_addHom` 📖	mathematical	—	`UniqueSums`	—	`uniqueAdd_of_nonempty` `Finset.Nonempty.image` `Finset.mem_image` `UniqueAdd.of_addHom_image`
`of_addOpposite` 📖	mathematical	—	`UniqueSums`	—	`AddOpposite.op_injective` `uniqueAdd_of_nonempty` `Finset.Nonempty.map` `Finset.mem_map'` `UniqueAdd.of_addOpposite`
`of_injective_addHom` 📖	mathematical	`DFunLike.coe` `AddHom` `AddHom.funLike`	`UniqueSums`	—	`of_addHom`
`of_same` 📖	mathematical	`Finset` `Finset.instMembership` `UniqueAdd` `AddSemigroup.toAdd`	`UniqueSums`	—	`Finset.Nonempty.add` `Finset.mem_add` `add_left_cancel` `IsCancelAdd.toIsLeftCancelAdd` `Finset.add_mem_add` `add_assoc` `add_right_cancel` `IsCancelAdd.toIsRightCancelAdd`
`toIsCancelAdd` 📖	mathematical	—	`IsCancelAdd`	—	`AddOpposite.op_injective` `IsLeftCancelAdd.add_left_cancel` `instAddOpposite` `AddOpposite.unop_injective`
`toTwoUniqueSums_of_addGroup` 📖	mathematical	—	`TwoUniqueSums` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`uniqueAdd_of_nonempty` `Finset.card_pos` `add_right_injective` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `Finset.card_map` `Finset.mem_map` `neg_add_cancel` `add_neg_cancel` `Finset.Nonempty.add` `Finset.Nonempty.image` `Finset.Nonempty.map` `Finset.mem_add` `Finset.mem_image` `add_assoc` `add_right_cancel_iff` `add_left_cancel_iff` `add_zero` `zero_add` `neg_add_rev` `Finset.exists_mem_ne` `neg_zero` `neg_eq_zero` `Finset.mem_product` `not_and_or` `add_neg_eq_zero` `neg_add_eq_zero` `Finset.mem_map_of_mem`
`uniqueAdd_of_nonempty` 📖	mathematical	`Finset.Nonempty`	`Finset` `Finset.instMembership` `UniqueAdd`	—	—

(root)

Definitions

Name	Category	Theorems
`TwoUniqueProds` 📖	CompData	12 math math: `TwoUniqueProds.instMulOpposite`, `TwoUniqueProds.of_injective_mulHom`, `TwoUniqueProds.of_covariant_right`, `Multiplicative.instTwoUniqueProdsOfTwoUniqueSums`, `FreeMonoid.instTwoUniqueProds`, `TwoUniqueProds.of_covariant_left`, `Prod.instTwoUniqueProds`, `TwoUniqueProds.of_mulOpposite`, `MulEquiv.twoUniqueProds_iff`, `UniqueProds.toTwoUniqueProds_of_group`, `AffineMonoid.to_twoUniqueProds`, `TwoUniqueProds.of_mulHom`
`TwoUniqueSums` 📖	CompData	15 math math: `AffineAddMonoid.to_twoUniqueSums`, `TwoUniqueSums.of_addHom`, `Additive.instTwoUniqueSumsOfTwoUniqueProds`, `TwoUniqueSums.of_covariant_right`, `instTwoUniqueSumsFinsupp`, `AddEquiv.twoUniqueSums_iff`, `TwoUniqueSums.of_addOpposite`, `TwoUniqueSums.of_covariant_left`, `TwoUniqueSums.instAddOpposite`, `instTwoUniqueSumsOfModuleRat`, `TwoUniqueSums.of_injective_addHom`, `FreeAddMonoid.instTwoUniqueSums`, `instTwoUniqueSumsFreeAbelianGroup`, `Prod.instTwoUniqueSums`, `UniqueSums.toTwoUniqueSums_of_addGroup`
`UniqueAdd` 📖	MathDef	10 math math: `UniqueAdd.of_subsingleton`, `UniqueAdd.iff_addOpposite`, `TwoUniqueSums.uniqueAdd_of_one_lt_card`, `UniqueAdd.exists_iff_exists_existsUnique`, `UniqueAdd.addHom_image_iff`, `UniqueAdd.addHom_map_iff`, `UniqueAdd.iff_card_le_one`, `UniqueSums.uniqueAdd_of_nonempty`, `UniqueAdd.of_card_le_one`, `UniqueAdd.iff_existsUnique`
`UniqueMul` 📖	MathDef	10 math math: `UniqueMul.exists_iff_exists_existsUnique`, `UniqueMul.mulHom_image_iff`, `TwoUniqueProds.uniqueMul_of_one_lt_card`, `UniqueMul.iff_existsUnique`, `UniqueProds.uniqueMul_of_nonempty`, `UniqueMul.iff_mulOpposite`, `UniqueMul.iff_card_le_one`, `UniqueMul.of_card_le_one`, `UniqueMul.of_subsingleton`, `UniqueMul.mulHom_map_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instTwoUniqueSumsDFinsupp` 📖	mathematical	`TwoUniqueSums` `AddZero.toAdd` `AddZeroClass.toAddZero`	`DFinsupp` `AddZero.toZero` `DFinsupp.instAdd`	—	`TwoUniqueSums.of_injective_addHom` `DFunLike.coe_injective` `TwoUniqueSums.instForall`
`instTwoUniqueSumsFinsupp` 📖	mathematical	—	`TwoUniqueSums` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `Finsupp.instAdd`	—	`TwoUniqueSums.of_injective_addHom` `DFunLike.coe_injective` `TwoUniqueSums.instForall`
`instUniqueSumsDFinsupp` 📖	mathematical	`UniqueSums` `AddZero.toAdd` `AddZeroClass.toAddZero`	`DFinsupp` `AddZero.toZero` `DFinsupp.instAdd`	—	`UniqueSums.of_injective_addHom` `DFunLike.coe_injective` `UniqueSums.instForall`
`instUniqueSumsFinsupp` 📖	mathematical	—	`UniqueSums` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `Finsupp.instAdd`	—	`UniqueSums.of_injective_addHom` `DFunLike.coe_injective` `UniqueSums.instForall`
`uniqueAdd_of_twoUniqueAdd` 📖	—	`Finset` `Finset.instMembership` `SProd.sprod` `Finset.instSProd` `UniqueAdd` `Finset.Nonempty`	—	—	`UniqueAdd.of_card_le_one` `Finset.card_pos` `Mathlib.Tactic.Push.not_and_or_eq` `not_le` `Finset.mem_product`
`uniqueMul_of_twoUniqueMul` 📖	—	`Finset` `Finset.instMembership` `SProd.sprod` `Finset.instSProd` `UniqueMul` `Finset.Nonempty`	—	—	`UniqueMul.of_card_le_one` `Finset.card_pos` `Mathlib.Tactic.Push.not_and_or_eq` `Finset.mem_product`

---

← Back to Index