Theorems · Theorem · group theory

IsAddIndecomposable.baseOf_subset_pos

∀ {ι : Type u_1} {M : Type u_2} {S : Type u_4} [inst : AddMonoid M] [inst_1 : LinearOrder S] [inst_2 : AddMonoid S]
  (v : ι → M) (f : M →+ S), IsAddIndecomposable.baseOf v f ⊆ {i | 0 < f (v i)}

Defined in

Mathlib.Algebra.Group.Irreducible.Indecomposable

Cited by

2 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext

Assumes

AddMonoidLinearOrderAddMonoid