zpow_eq_zpow_iff_cases₀ — Mathlib

English

Let α be a linearly ordered field with IsStrictOrderedRing. For any a,b ∈ α and any n ∈ ℤ, a^n = b^n iff n = 0 or a = b or a = -b and Even n.

Русский

Пусть α — упорядоченное поле с IsStrictOrderedRing. Для любых a,b ∈ α и n ∈ ℤ, a^n = b^n тогда и только если n = 0 или a = b или a = −b и n чётно.

LaTeX

$$$\forall a,b \in \alpha, \forall n \in \mathbb{Z} \, (a^{n} = b^{n}) \iff (n = 0) \lor (a = b) \lor (a = -b \land \mathrm{Even}(n))$$$

Lean4

theorem zpow_eq_zpow_iff_cases₀ : a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n := by
  rcases eq_or_ne n 0 with rfl | hn <;> simp [zpow_eq_zpow_iff_of_ne_zero₀, *]

Похожие утверждения