English
If w is congruent to x, then w^n is congruent to x^n for every natural n.
Русский
Если w относится к x по конгруэнции, то w^n относится к x^n для любого натурального n.
LaTeX
$$$\\forall n\\in\\mathbb{N},\ c\ \\,w\,x \\Rightarrow c\\,(w^n)\\,(x^n)$$$
Lean4
/-- Multiplicative congruence relations preserve natural powers. -/
@[to_additive /-- Additive congruence relations preserve natural scaling. -/
]
protected theorem pow {M : Type*} [Monoid M] (c : Con M) : ∀ (n : ℕ) {w x}, c w x → c (w ^ n) (x ^ n)
| 0, w, x, _ => by simpa using c.refl _
| Nat.succ n, w, x, h => by simpa [pow_succ] using c.mul (Con.pow c n h) h
