English
The RatFunc.mk construction is compatible with scalar multiplication: for any c ∈ R and p,q ∈ K[X], RatFunc.mk (c • p) q = c • RatFunc.mk p q.
Русский
Конструкция RatFunc.mk совместима со скалярным умножением: для любых c ∈ R и p,q ∈ K[X], RatFunc.mk (c • p) q = c • RatFunc.mk p q.
LaTeX
$$$\forall c\in R, \forall p,q\in K[X],\; \mathrm{RatFunc}.mk (c \cdot p) q = c \cdot \mathrm{RatFunc}.mk p q$$$
Lean4
theorem mk_smul (c : R) (p q : K[X]) : RatFunc.mk (c • p) q = c • RatFunc.mk p q :=
by
letI : SMulZeroClass R (FractionRing K[X]) := inferInstance
by_cases hq : q = 0
· rw [hq, mk_zero, mk_zero, ← ofFractionRing_smul, smul_zero]
· rw [mk_eq_localization_mk _ hq, mk_eq_localization_mk _ hq, ← Localization.smul_mk, ← ofFractionRing_smul]
