English
If a property holds for 1 and is preserved under left multiplication by g and left multiplication by g^{-1}, then it holds for all powers g^n.
Русский
Если свойство верно для 1 и сохраняется при левом умножении на g и на g^{-1}, то оно верно для всех степеней g^n.
LaTeX
$$$\forall P:\, G\to \mathrm{Prop},\ P(1) \land (\forall a\in G, P(a)\to P(g a)) \land (\forall a\in G, P(a)\to P(g^{-1} a)) \Rightarrow \forall n \in \mathbb{Z},\ P(g^{n})$$$
Lean4
/-- 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`. -/
@[to_additive /-- 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`. -/
]
theorem zpow_induction_left {g : G} {P : G → Prop} (h_one : P (1 : G)) (h_mul : ∀ a, P a → P (g * a))
(h_inv : ∀ a, P a → P (g⁻¹ * a)) (n : ℤ) : P (g ^ n) := by
induction n with
| zero => rwa [zpow_zero]
| succ n ih =>
rw [Int.add_comm, zpow_add, zpow_one]
exact h_mul _ ih
| pred n ih =>
rw [Int.sub_eq_add_neg, Int.add_comm, zpow_add, zpow_neg_one]
exact h_inv _ ih
