Theorems · Theorem · group theory

AddSubgroup.closure_induction

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

An induction principle for additive closure membership. If p holds for 0 and all elements of k, and is preserved under addition and inverses, then p holds for all elements of the additive closure of k. See also AddSubgroup.closure_induction_left and AddSubgroup.closure_induction_left for versions that only require showing p is preserved by addition by elements in k.

Defined in

Mathlib.Algebra.Group.Subgroup.Lattice

Cited by

14 results in Mathlib

Foundations

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

Assumes

AddGroup