val_pow — Mathlib

English

Exponentiation is compatible with val: (y^n).val = (y.val)^n for all y and n.

Русский

Возведение в степень совместимо с val: (y^n).val = (y.val)^n для всех y и n.

LaTeX

$$$\\forall y \\in \\mathrm{HomogeneousLocalization}(\\mathcal{A},x),\\; \\forall n \\in \\mathbb{N},\\; (y^n).\\mathrm{val} = (y.\\mathrm{val})^n$$$

Lean4

@[simp]
theorem val_pow : ∀ (y : HomogeneousLocalization 𝒜 x) (n : ℕ), (y ^ n).val = y.val ^ n :=
  Quotient.ind' fun y n ↦ by rw [← mk_pow, val_mk, val_mk, Localization.mk_pow]; rfl

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