Theorems · Theorem · group theory

zsmul_induction_right

∀ {G : Type u_3} [inst : AddGroup G] {g : G} {P : G → Prop},
  P 0 → (∀ (a : G), P a → P (a + g)) → (∀ (a : G), P a → P (a + -g)) → ∀ (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 right. For additive subgroups generated by more than one element, see AddSubgroup.closure_induction_right.

Defined in

Mathlib.Algebra.Group.Basic

Cited by

1 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext

Assumes

AddGroup