coe_pow — Mathlib

English

For any natural n and r in R, the coercion of r^n equals the n-th power in QuadraticAlgebra R a b.

Русский

Для любого n≥0 и r∈R, коэффициент r^n в QuadraticAlgebra R a b равен r^n как элемент квадратичной алгебры.

LaTeX

$$$((r^n : R) : \QuadraticAlgebra R a b) = (r : \QuadraticAlgebra R a b)^n$$$

Lean4

@[norm_cast, simp]
theorem coe_pow (n : ℕ) (r : R) : ((r ^ n : R) : QuadraticAlgebra R a b) = (r : QuadraticAlgebra R a b) ^ n :=
  (algebraMap R (QuadraticAlgebra R a b)).map_pow r n

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