zpow_abs — Mathlib

English

Let α be a linearly ordered field with IsStrictOrderedRing. If p is an even integer, then |a|^p = a^p for all a ∈ α.

Русский

Пусть α — упорядоченное поле с IsStrictOrderedRing. Если p чётно, то |a|^p = a^p для всех a ∈ α.

LaTeX

$$$\forall a \in \alpha, \text{ Even}(p) \Rightarrow |a|^{p} = a^{p}$ $$

Lean4

theorem zpow_abs {p : ℤ} (hp : Even p) (a : α) : |a| ^ p = a ^ p := by
  rcases abs_choice a with h | h <;> simp only [h, hp.neg_zpow _]

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