Theorems · Theorem · group theory

IsMulIndecomposable.baseOf_subset_one_lt

∀ {ι : Type u_1} {M : Type u_2} {S : Type u_4} [inst : Monoid M] [inst_1 : LinearOrder S] [inst_2 : Monoid S]
  (v : ι → M) (f : M →* S), IsMulIndecomposable.baseOf v f ⊆ {i | 1 < 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

MonoidLinearOrderMonoid