Theorems · Theorem · group theory

zpow_induction_left

∀ {G : Type u_3} [inst : Group G] {g : G} {P : G → Prop},
  P 1 → (∀ (a : G), P a → P (g * a)) → (∀ (a : G), P a → P (g⁻¹ * a)) → ∀ (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 left. For subgroups generated by more than one element, see Subgroup.closure_induction_left.

Defined in

Mathlib.Algebra.Group.Basic

Cited by

0 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext

Assumes

Group