English
Congruences preserve integer powers: if w ≡ x, then w^n ≡ x^n for any integer n.
Русский
Конгруэнции сохраняют целочисленные степени: если w ≡ x, то w^n ≡ x^n для любого целого n.
LaTeX
$$$\\forall n \\in \\mathbb{Z},\\ c\\,w\\,x \\Rightarrow c\\,(w^n)\\,(x^n)$$$
Lean4
/-- Multiplicative congruence relations preserve integer powers. -/
@[to_additive /-- Additive congruence relations preserve integer scaling. -/
]
protected theorem zpow : ∀ (n : ℤ) {w x}, c w x → c (w ^ n) (x ^ n)
| Int.ofNat n, w, x, h => by simpa only [zpow_natCast, Int.ofNat_eq_coe] using c.pow n h
| Int.negSucc n, w, x, h => by simpa only [zpow_negSucc] using c.inv (c.pow _ h)
