val_pow — Mathlib

English

For x in the positive subtype of a ring and n ∈ N, the coercion preserves exponentiation: ↑(x^n) = (↑x)^n.

Русский

Для x ∈ положительного подтипа кольца и n ∈ N справедливо: ↑(x^n) = (↑x)^n.

LaTeX

$$$\\\\forall x \\\\in \\\\{ x : R \\\\mid 0 < x \\\\},\\\\forall n \\\\in \\\\mathbb{N}, \\\\ ↑(x^n) = (↑x)^n.$$$

Lean4

@[simp]
theorem val_pow (x : { x : R // 0 < x }) (n : ℕ) : ↑(x ^ n) = (x : R) ^ n :=
  rfl

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