Theorems · Theorem · group theory

zsmul_induction_left

∀ {G : Type u_3} [inst : AddGroup G] {g : G} {P : G → Prop},
  P 0 → (∀ (a : G), P a → P (g + a)) → (∀ (a : G), P a → P (-g + a)) → ∀ (n : ℤ), P (n • g)

To show a property of all multiples of g it suffices to show it is closed under addition by g and -g on the left. For additive subgroups generated by more than one element, see AddSubgroup.closure_induction_left.

Defined in

Mathlib.Algebra.Group.Basic

Cited by

0 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext

Assumes

AddGroup