English
A specialized instance asserts that RatFunc inherits faithful scalar action from a base polynomial ring; i.e., RatFunc can be viewed as a faithfully acting module in the polynomial context.
Русский
Специальный экземпляр утверждает, что RatFunc наследует достоверное скалярное действие от базового кольца полиномов; RatFunc рассматривается как модуль с подтвержденным действием.
LaTeX
$$$\text{FaithfulSMul } K[X] \text{ on } RatFunc E$$$
Lean4
/-- `FractionRing.instFaithfulSMul` specialized to `RatFunc R`. -/
instance faithfulSMul (K E : Type*) [Field K] [Field E] [Algebra K E] [FaithfulSMul K E] :
FaithfulSMul K[X] (RatFunc E) :=
(faithfulSMul_iff_algebraMap_injective ..).mpr <|
(IsFractionRing.injective E[X] _).comp (Polynomial.map_injective _ <| FaithfulSMul.algebraMap_injective K E)
