Theorems · Theorem · group theory

RootPairing.weylGroup.induction

∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  {pred : (g : P.Aut) → g ∈ P.weylGroup → Prop},
  (∀ (i : ι), pred (RootPairing.Equiv.reflection P i) ⋯) →
    pred 1 ⋯ →
      (∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯) →
        ∀ {x : P.Aut} (hx : x ∈ P.weylGroup), pred x hx

Defined in

Mathlib.LinearAlgebra.RootSystem.WeylGroup

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleAddCommGroupModule