Theorems · Theorem · group theory

AddSubgroup.closure_induction_left

∀ {G : Type u_2} [inst : AddGroup G] {s : Set G} {p : (x : G) → x ∈ AddSubgroup.closure s → Prop},
  p 0 ⋯ →
    (∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ AddSubgroup.closure s), p y hy → p (x + y) ⋯) →
      (∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ AddSubgroup.closure s), p y hy → p (-x + y) ⋯) →
        ∀ {x : G} (h : x ∈ AddSubgroup.closure s), p x h

For additive subgroups generated by a single element, see the simpler zsmul_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

AddGroup