ofFractionRing_comp_algebraMap — Mathlib

English

The canonical embedding of polynomials into RatFunc is compatible with the fraction ring through the fraction map: ofFractionRing ∘ algebraMap K[X] (FractionRing K[X]) = algebraMap K[X] (RatFunc K).

Русский

Каноническое включение многочленов в RatFunc совместимо с окружением дробей: ofFractionRing ∘ algebraMap K[X] (FractionRing K[X]) = algebraMap K[X] (RatFunc K).

LaTeX

$$$ \operatorname{ofFractionRing} \circ \operatorname{algebraMap}_{K[X], \ FractionRing(K[X])} = \operatorname{algebraMap}_{K[X], \ RatFunc(K)}$$$

Lean4

theorem ofFractionRing_comp_algebraMap : ofFractionRing ∘ algebraMap K[X] (FractionRing K[X]) = algebraMap _ _ :=
  funext ofFractionRing_algebraMap

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