English
If a property holds for 1 and is preserved under right multiplication by g and 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(a g)) \land (\forall a\in G, P(a)\to P(a g^{-1})) \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 right. For subgroups generated by more than one element, see
`Subgroup.closure_induction_right`. -/
@[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 right. For additive subgroups generated by more than one element,
see `AddSubgroup.closure_induction_right`. -/
]
theorem zpow_induction_right {g : G} {P : G → Prop} (h_one : P (1 : G)) (h_mul : ∀ a, P a → P (a * g))
(h_inv : ∀ a, P a → P (a * g⁻¹)) (n : ℤ) : P (g ^ n) := by
induction n with
| zero => rwa [zpow_zero]
| succ n ih =>
rw [zpow_add_one]
exact h_mul _ ih
| pred n ih =>
rw [zpow_sub_one]
exact h_inv _ ih
