English
Let α be a linearly ordered field with IsStrictOrderedRing. For any a,b ∈ α and any n ∈ ℤ with n ≠ 0, a^n = b^n iff a = b or a = -b and Even n.
Русский
Пусть α — упорядоченное поле с IsStrictOrderedRing. Для любых a,b ∈ α и n ∈ ℤ при n ≠ 0 верно: a^n = b^n тогда и только если a = b или a = −b и n чётно.
LaTeX
$$$\forall a,b \in \alpha, \forall n \in \mathbb{Z}, n \ne 0 \Rightarrow a^{n} = b^{n} \\iff (a = b) \lor (a = -b \land \mathrm{Even}(n))$$$
Lean4
theorem zpow_eq_zpow_iff_of_ne_zero₀ (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n :=
match n with
| Int.ofNat m =>
by
simp only [Int.ofNat_eq_coe, ne_eq, Nat.cast_eq_zero, zpow_natCast, Int.even_coe_nat] at *
exact pow_eq_pow_iff_of_ne_zero hn
| Int.negSucc m =>
by
simp only [← neg_ofNat_succ, ne_eq, neg_eq_zero, Nat.cast_eq_zero, zpow_neg, zpow_natCast, inv_inj, even_neg,
Int.even_coe_nat] at *
exact pow_eq_pow_iff_of_ne_zero hn
