Theorems · Theorem · group theory

Subgroup.closure_induction_left

∀ {G : Type u_2} [inst : Group G] {s : Set G} {p : (x : G) → x ∈ Subgroup.closure s → Prop},
  p 1 ⋯ →
    (∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Subgroup.closure s), p y hy → p (x * y) ⋯) →
      (∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Subgroup.closure s), p y hy → p (x⁻¹ * y) ⋯) →
        ∀ {x : G} (h : x ∈ Subgroup.closure s), p x h

For subgroups generated by a single element, see the simpler zpow_induction_left.

Defined in

Mathlib.Algebra.Group.Subgroup.Pointwise

Cited by

2 results in Mathlib

Foundations

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

Assumes

Group