English
There is a faithful scalar multiplication structure on RatFunc by polynomials over any field R, i.e., RatFunc E is a faithful module over Polynomial E, which in particular implies injectivity of algebra maps from polynomial rings.
Русский
Задано верное действует скалярное умножение на RatFunc E по полиномам над E; RatFunc E — достоверно модуль над Polynomial E.
LaTeX
$$$\text{FaithfulSMul} \; K[X] \; (\text{RatFunc } E)$$$
Lean4
/-- `FractionRing.liftAlgebra` specialized to `RatFunc R`.
This is a scoped instance because it creates a diamond when `L = RatFunc R`. -/
scoped instance liftAlgebra : Algebra (RatFunc R) L :=
RingHom.toAlgebra (IsFractionRing.lift (FaithfulSMul.algebraMap_injective R[X] _))
