Documentation Verification Report

Indecomposable

📁 Source: Mathlib/Algebra/Group/Irreducible/Indecomposable.lean

Statistics

Metric	Count
Definitions `Indecomposable`, `IsAddIndecomposable`, `baseOf`, `IsMulIndecomposable`, `baseOf`	5
Theorems `closure_image_isAddIndecomposable_baseOf`, `apply_ne_zero_of_mem_or_neg_mem_closure`, `closure_image_isAddIndecomposable_baseOf`, `mem_closure_image_pos_iff`, `apply_ne_zero_iff_mem_closure`, `baseOf_subset_pos`, `image_baseOf_neg_comp_eq`, `mem_or_neg_mem_closure_baseOf`, `pairwise_baseOf_sub_notMem`, `pairwise_sub_notMem_range`, `pairwise_sub_notMem_range'`, `subset`, `apply_ne_one_iff_mem_closure`, `baseOf_subset_one_lt`, `image_baseOf_inv_comp_eq`, `mem_or_inv_mem_closure_baseOf`, `pairwise_baseOf_div_notMem`, `pairwise_div_notMem_range`, `pairwise_div_notMem_range'`, `subset`, `closure_image_isMulIndecomposable_baseOf`, `apply_ne_one_of_mem_or_inv_mem_closure`, `closure_image_isMulIndecomposable_baseOf`, `closure_image_one_lt_and_isMulIndecomposable`, `mem_closure_image_one_lt_iff`, `isAddIndecomposable_id_univ`, `isMulIndecomposable_id_univ`	27
Total	32

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_image_isAddIndecomposable_baseOf` 📖	mathematical	`InvolutiveNeg.toNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`closure` `AddCommGroup.toAddGroup` `Set.image` `IsAddIndecomposable.baseOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Set.range`	—	`Set.image_univ` `le_antisymm` `closure_mono` `Set.image_mono` `Set.subset_univ` `closure_le` `Set.ext` `Set.mem_univ` `Set.mem_union` `lt_or_lt_iff_ne` `Set.image_union` `Set.union_subset_iff` `le_trans` `AddSubmonoid.closure_image_isAddIndecomposable_baseOf` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `AddSubmonoid.subset_closure` `le_closure_toAddSubmonoid` `Set.image_comp` `IsAddIndecomposable.image_baseOf_neg_comp_eq` `Set.image_congr` `neg_neg` `Set.image_id'` `Left.neg_pos_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `coe_negAddMonoidHom` `Set.image_neg_eq_neg` `closure_neg`

AddSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_ne_zero_of_mem_or_neg_mem_closure` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `InvolutiveNeg.toNeg` `NegZeroClass.toNeg` `AddSubmonoid` `SetLike.instMembership` `instSetLike` `closure` `Set.image`	—	—	`closure_induction` `Set.mem_image` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `lt_self_iff_false` `eq_or_ne` `map_add` `AddMonoidHomClass.toAddHomClass` `lt_add_of_lt_of_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `LT.lt.ne'` `map_neg` `neg_eq_zero` `neg_neg`
`closure_image_isAddIndecomposable_baseOf` 📖	mathematical	—	`closure` `AddMonoid.toAddZeroClass` `Set.image` `IsAddIndecomposable.baseOf` `AddCommMonoid.toAddMonoid` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike`	—	`le_antisymm` `closure_mono` `Set.image_mono` `IsAddIndecomposable.baseOf_subset_pos` `closure_le` `Set.Finite.exists_minimalFor` `instIsTransLe` `Set.toFinite` `Subtype.finite` `MinimalFor.prop` `not_le` `MinimalFor.le_of_le` `LT.lt.le` `Mathlib.Tactic.Contrapose.contrapose₄` `subset_closure` `Set.mem_image_of_mem` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `lt_add_iff_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `lt_add_iff_pos_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `contravariant_swap_add_of_contravariant_add` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `instAddSubmonoidClass`
`mem_closure_image_pos_iff` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `closure` `Set.image` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike`	—	`closure_induction` `Set.mem_image` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `lt_self_iff_false` `zero_add` `add_zero` `map_add` `AddMonoidHomClass.toAddHomClass` `Left.add_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `subset_closure` `Set.mem_image_of_mem`

CategoryTheory

Definitions

Name	Category	Theorems
`Indecomposable` 📖	MathDef	1 math math: `indecomposable_of_simple`

IsAddIndecomposable

Definitions

Name	Category	Theorems
`baseOf` 📖	CompOp	13 math math: `image_baseOf_neg_comp_eq`, `RootPairing.linearIndepOn_root_baseOf'`, `AddSubmonoid.closure_image_isAddIndecomposable_baseOf`, `AddSubgroup.closure_image_isAddIndecomposable_baseOf`, `RootPairing.linearIndepOn_root_baseOf`, `RootPairing.eq_baseOf_of_linearIndepOn_of_mem_or_neg_mem_closure`, `apply_ne_zero_iff_mem_closure`, `RootPairing.eq_baseOf_iff`, `mem_or_neg_mem_closure_baseOf`, `pairwise_baseOf_sub_notMem`, `baseOf_subset_pos`, `RootPairing.baseOf_pairwise_pairing_le_zero`, `RootPairing.baseOf_root_eq_baseOf_coroot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_ne_zero_iff_mem_closure` 📖	mathematical	`InvolutiveNeg.toNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `Set.image` `baseOf`	—	`mem_or_neg_mem_closure_baseOf` `AddSubmonoid.apply_ne_zero_of_mem_or_neg_mem_closure` `baseOf_subset_pos`
`baseOf_subset_pos` 📖	mathematical	—	`Set` `Set.instHasSubset` `baseOf` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike`	—	`subset`
`image_baseOf_neg_comp_eq` 📖	mathematical	`InvolutiveNeg.toNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Set.image` `baseOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubtractionMonoid.toSubNegMonoid` `AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `negAddMonoidHom` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike`	—	`map_neg` `AddMonoidHom.instAddMonoidHomClass` `Left.neg_pos_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `neg_add` `neg_eq_iff_eq_neg` `neg_eq_zero` `Left.neg_neg_iff` `neg_neg` `subset_antisymm` `Set.instAntisymmSubset` `Set.image_mono` `Set.image_congr` `Set.image_subset_iff` `Set.image_id'` `Set.image_comp` `negAddMonoidHom_comp_negAddMonoidHom` `AddMonoidHom.coe_comp` `AddMonoidHom.id_comp` `AddMonoidHom.comp_assoc`
`mem_or_neg_mem_closure_baseOf` 📖	mathematical	`InvolutiveNeg.toNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure` `Set.image` `baseOf`	—	`AddSubmonoid.closure_image_isAddIndecomposable_baseOf` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `lt_or_gt_of_ne` `AddSubmonoid.subset_closure` `map_neg` `AddMonoidHom.instAddMonoidHomClass` `Left.neg_pos_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono`
`pairwise_baseOf_sub_notMem` 📖	mathematical	`InvolutiveNeg.toNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Set.Pairwise` `baseOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Set` `Set.instMembership` `Set.range` `SubNegMonoid.toSub`	—	`pairwise_sub_notMem_range'` `Set.Subset.refl`
`pairwise_sub_notMem_range` 📖	mathematical	`InvolutiveNeg.toNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.instHasSubset` `setOf` `IsAddIndecomposable` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Set.instMembership`	`Set.Pairwise` `Set.range` `SubNegMonoid.toSub`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset` `sub_add_cancel` `neg_sub`
`pairwise_sub_notMem_range'` 📖	mathematical	`InvolutiveNeg.toNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.instHasSubset` `setOf` `IsAddIndecomposable` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	`Set.Pairwise` `Set.instMembership` `Set.range` `SubNegMonoid.toSub`	—	`Mathlib.Tactic.Contrapose.contrapose₃` `Mathlib.Tactic.Push.not_forall_eq` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `pairwise_sub_notMem_range` `map_neg` `Left.neg_pos_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `lt_or_lt_iff_ne`
`subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `setOf` `IsAddIndecomposable`	—	`Set.sep_subset`

IsMulIndecomposable

Definitions

Name	Category	Theorems
`baseOf` 📖	CompOp	8 math math: `pairwise_baseOf_div_notMem`, `Subgroup.closure_image_isMulIndecomposable_baseOf`, `mem_or_inv_mem_closure_baseOf`, `image_baseOf_inv_comp_eq`, `baseOf_subset_one_lt`, `Submonoid.closure_image_isMulIndecomposable_baseOf`, `Submonoid.closure_image_one_lt_and_isMulIndecomposable`, `apply_ne_one_iff_mem_closure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_ne_one_iff_mem_closure` 📖	mathematical	`InvolutiveInv.toInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.closure` `Set.image` `baseOf`	—	`mem_or_inv_mem_closure_baseOf` `Submonoid.apply_ne_one_of_mem_or_inv_mem_closure` `baseOf_subset_one_lt`
`baseOf_subset_one_lt` 📖	mathematical	—	`Set` `Set.instHasSubset` `baseOf` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DFunLike.coe` `MonoidHom` `MonoidHom.instFunLike`	—	`subset`
`image_baseOf_inv_comp_eq` 📖	mathematical	`InvolutiveInv.toInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`Set.image` `baseOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `DivisionMonoid.toDivInvMonoid` `MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `invMonoidHom` `DFunLike.coe` `MonoidHom` `MonoidHom.instFunLike`	—	`map_inv` `MonoidHom.instMonoidHomClass` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `LeftCancelSemigroup.toIsLeftCancelMul` `IsOrderedMonoid.toMulLeftMono` `mul_inv` `inv_eq_iff_eq_inv` `inv_inv` `subset_antisymm` `Set.instAntisymmSubset` `Set.image_mono` `Set.image_congr` `Set.image_id'` `Set.image_comp` `invMonoidHom_comp_invMonoidHom` `MonoidHom.coe_comp` `MonoidHom.id_comp` `MonoidHom.comp_assoc`
`mem_or_inv_mem_closure_baseOf` 📖	mathematical	`InvolutiveInv.toInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`Submonoid` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.closure` `Set.image` `baseOf`	—	`Submonoid.closure_image_isMulIndecomposable_baseOf` `IsOrderedMonoid.toIsOrderedCancelMonoid` `lt_or_gt_of_ne` `Submonoid.subset_closure` `map_inv` `MonoidHom.instMonoidHomClass` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `LeftCancelSemigroup.toIsLeftCancelMul` `IsOrderedMonoid.toMulLeftMono`
`pairwise_baseOf_div_notMem` 📖	mathematical	`InvolutiveInv.toInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`Set.Pairwise` `baseOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Set` `Set.instMembership` `Set.range` `DivInvMonoid.toDiv`	—	`pairwise_div_notMem_range'` `Set.Subset.refl`
`pairwise_div_notMem_range` 📖	mathematical	`InvolutiveInv.toInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Set` `Set.instHasSubset` `setOf` `IsMulIndecomposable` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Set.instMembership`	`Set.Pairwise` `Set.range` `DivInvMonoid.toDiv`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset` `div_mul_cancel` `inv_div`
`pairwise_div_notMem_range'` 📖	mathematical	`InvolutiveInv.toInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Set` `Set.instHasSubset` `setOf` `IsMulIndecomposable` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `InvOneClass.toOne` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike`	`Set.Pairwise` `Set.instMembership` `Set.range` `DivInvMonoid.toDiv`	—	`Mathlib.Tactic.Contrapose.contrapose₃` `Mathlib.Tactic.Push.not_forall_eq` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass` `pairwise_div_notMem_range` `map_inv` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `LeftCancelSemigroup.toIsLeftCancelMul` `IsOrderedMonoid.toMulLeftMono`
`subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `setOf` `IsMulIndecomposable`	—	—

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_image_isMulIndecomposable_baseOf` 📖	mathematical	`InvolutiveInv.toInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`closure` `CommGroup.toGroup` `Set.image` `IsMulIndecomposable.baseOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Set.range`	—	`Set.image_univ` `le_antisymm` `closure_mono` `Set.image_mono` `closure_le` `Set.ext` `Set.image_union` `Set.union_subset_iff` `le_trans` `Submonoid.closure_image_isMulIndecomposable_baseOf` `IsOrderedMonoid.toIsOrderedCancelMonoid` `le_closure_toSubmonoid` `Set.image_comp` `IsMulIndecomposable.image_baseOf_inv_comp_eq` `Set.image_congr` `inv_inv` `Set.image_id'` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `LeftCancelSemigroup.toIsLeftCancelMul` `IsOrderedMonoid.toMulLeftMono` `coe_invMonoidHom` `Set.image_inv_eq_inv` `closure_inv`

Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_ne_one_of_mem_or_inv_mem_closure` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MonoidHom.instFunLike` `InvolutiveInv.toInv` `InvOneClass.toInv` `Submonoid` `SetLike.instMembership` `instSetLike` `closure` `Set.image`	—	—	`closure_induction` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass` `eq_or_ne` `map_mul` `MonoidHomClass.toMulHomClass` `lt_mul_of_lt_of_one_lt` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `LeftCancelSemigroup.toIsLeftCancelMul` `IsOrderedMonoid.toMulLeftMono` `LT.lt.ne'` `map_inv` `inv_inv`
`closure_image_isMulIndecomposable_baseOf` 📖	mathematical	—	`closure` `Monoid.toMulOneClass` `Set.image` `IsMulIndecomposable.baseOf` `CommMonoid.toMonoid` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toOne` `MulOneClass.toMulOne` `DFunLike.coe` `MonoidHom` `MonoidHom.instFunLike`	—	`le_antisymm` `closure_mono` `Set.image_mono` `IsMulIndecomposable.baseOf_subset_one_lt` `closure_le` `Set.Finite.exists_minimalFor` `instIsTransLe` `Set.toFinite` `Subtype.finite` `MinimalFor.prop` `not_le` `MinimalFor.le_of_le` `LT.lt.le` `Mathlib.Tactic.Contrapose.contrapose₄` `subset_closure` `Set.mem_image_of_mem` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `IsCancelMul.toIsLeftCancelMul` `IsOrderedCancelMonoid.toIsCancelMul` `IsOrderedMonoid.toMulLeftMono` `IsOrderedCancelMonoid.toIsOrderedMonoid` `contravariant_lt_of_covariant_le` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `IsCancelMul.toIsRightCancelMul` `covariant_swap_mul_of_covariant_mul` `contravariant_swap_mul_of_contravariant_mul` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `instSubmonoidClass`
`closure_image_one_lt_and_isMulIndecomposable` 📖	mathematical	—	`closure` `Monoid.toMulOneClass` `Set.image` `IsMulIndecomposable.baseOf` `CommMonoid.toMonoid` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toOne` `MulOneClass.toMulOne` `DFunLike.coe` `MonoidHom` `MonoidHom.instFunLike`	—	`closure_image_isMulIndecomposable_baseOf`
`mem_closure_image_one_lt_iff` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `closure` `Set.image` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toOne` `MulOneClass.toMulOne` `CommMonoid.toMonoid` `DFunLike.coe` `MonoidHom` `MonoidHom.instFunLike`	—	`closure_induction` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass` `one_mul` `mul_one` `map_mul` `MonoidHomClass.toMulHomClass` `Left.one_lt_mul` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `IsCancelMul.toIsLeftCancelMul` `IsOrderedCancelMonoid.toIsCancelMul` `IsOrderedMonoid.toMulLeftMono` `IsOrderedCancelMonoid.toIsOrderedMonoid` `subset_closure` `Set.mem_image_of_mem`

(root)

Definitions

Name	Category	Theorems
`IsAddIndecomposable` 📖	MathDef	2 math math: `isAddIndecomposable_id_univ`, `IsAddIndecomposable.subset`
`IsMulIndecomposable` 📖	MathDef	2 math math: `IsMulIndecomposable.subset`, `isMulIndecomposable_id_univ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddIndecomposable_id_univ` 📖	mathematical	—	`IsAddIndecomposable` `Set.univ` `AddIrreducible`	—	`isAddUnit_iff_eq_zero` `Set.mem_univ` `AddIrreducible.isAddUnit_or_isAddUnit`
`isMulIndecomposable_id_univ` 📖	mathematical	—	`IsMulIndecomposable` `Set.univ` `Irreducible`	—	`Irreducible.isUnit_or_isUnit`

---

← Back to Index