Theorems · Theorem · group theory

IsMulIndecomposable.mem_or_inv_mem_closure_baseOf

∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S] [Finite ι]
  [inst_3 : InvolutiveInv ι] [inst_4 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (i : ι),
  f (v i) ≠ 1 →
    v i⁻¹ = (v i)⁻¹ →
      v i ∈ Submonoid.closure (v '' IsMulIndecomposable.baseOf v f) ∨
        (v i)⁻¹ ∈ Submonoid.closure (v '' IsMulIndecomposable.baseOf v f)

Defined in

Mathlib.Algebra.Group.Irreducible.Indecomposable

Cited by

1 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommGroupLinearOrderFiniteInvolutiveInvCommGroupIsOrderedMonoid