mk_one — Mathlib

English

For any polynomial x in K[X], RatFunc.mk x 1 equals algebraMap x, i.e., the canonical embedding sends polynomials to RatFunc faithfully.

Русский

Для любого многочлена x ∈ K[X], RatFunc.mk x 1 равно algebraMap x, то есть каноническое вложение отображает многочлены в RatFunc корректно.

LaTeX

$$$\\text{RatFunc}.mk(x,1)=\\text{algebraMap }(K[X],\\text{RatFunc}K)(x)$$$

Lean4

theorem mk_one (x : K[X]) : RatFunc.mk x 1 = algebraMap _ _ x :=
  rfl

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