invFun_monomial

Mathlib.RingTheory.PolynomialAlgebra

URI: https://scilib.ai/kg/mathlib#PolyEquivTensor.invFun_monomial

English

For n ∈ N and a ∈ A, invFun of a monomial equals (a ⊗ 1) ⋅ (1 ⊗ X)^n.

Русский

Для n ∈ N и a ∈ A, invFun( мономиал n a ) = (a ⊗ 1) ⋅ (1 ⊗ X)^n.

LaTeX

$$invFun_R A( monomial n a ) = (a \\otimes 1) * (1 \\otimes X)^n$$

Lean4

theorem invFun_monomial (n : ℕ) (a : A) : invFun R A (monomial n a) = (a ⊗ₜ[R] 1) * 1 ⊗ₜ[R] X ^ n :=
  eval₂_monomial _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru