algebraMap_injective — Mathlib

English

The natural map from F_q[X] to F (via the tower) is injective; i.e., the polynomial ring embeds into F.

Русский

Естественная карта из F_q[X] в F инъективна; полиномиальная кольцо вкладывается в F.

LaTeX

$$$\\big(\\mathrm{algebraMap}\\,F_q[X]\\,F\\big)\\;\\text{injective}$$$

Lean4

theorem algebraMap_injective [Algebra Fq[X] F] [Algebra (RatFunc Fq) F] [IsScalarTower Fq[X] (RatFunc Fq) F] :
    Function.Injective (⇑(algebraMap Fq[X] F)) :=
  by
  rw [IsScalarTower.algebraMap_eq Fq[X] (RatFunc Fq) F]
  exact (algebraMap (RatFunc Fq) F).injective.comp (IsFractionRing.injective Fq[X] (RatFunc Fq))

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