Theorems · Theorem · group theory

zpow_induction_right

∀ {G : Type u_3} [inst : Group G] {g : G} {P : G → Prop},
  P 1 → (∀ (a : G), P a → P (a * g)) → (∀ (a : G), P a → P (a * g⁻¹)) → ∀ (n : ℤ), P (g ^ n)

To show a property of all powers of g it suffices to show it is closed under multiplication by g and g⁻¹ on the right. For subgroups generated by more than one element, see Subgroup.closure_induction_right.

Defined in

Mathlib.Algebra.Group.Basic

Cited by

1 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext

Assumes

Group