mk_pow — Mathlib

English

There is a natural power operation on HomogeneousLocalization 𝒜 x, i.e., an instance of Pow with Natural numbers.

Русский

Существует естественная операция возведения в степень на HomogeneousLocalization 𝒜 x, то есть инстанс Pow над натуральными числами.

LaTeX

$$$\text{Pow} (\mathrm{HomogeneousLocalization}_{\mathcal{A}}(x)) \mathbb{N}$$$

Lean4

@[simp]
theorem mk_pow (i : NumDenSameDeg 𝒜 x) (n : ℕ) : mk (i ^ n) = mk i ^ n :=
  rfl

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