Theorems · Theorem · group theory

IsMulIndecomposable.apply_ne_one_iff_mem_closure

∀ {ι : 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 : ι),
  v i ≠ 1 →
    v i⁻¹ = (v i)⁻¹ →
      (f (v i) ≠ 1 ↔
        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

0 results in Mathlib

Foundations

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

Assumes

CommGroupLinearOrderFiniteInvolutiveInvCommGroupIsOrderedMonoid