English
If S acts on N compatibly with R via an SMulCommClass, then S acts on QuadraticMap R M N compatibly: a • (Q + Q') = a • Q + a • Q', (a b) • Q = a • (b • Q), 1 • Q = Q, a • 0 = 0.
Русский
Если S действует на N совместимо с R через SMulCommClass, то S действует на QuadraticMap R M N совместимо: a · (Q+Q') = a · Q + a · Q', (a b) · Q = a · (b · Q), 1 · Q = Q, a · 0 = 0.
LaTeX
$$$\\forall a\\in S:\\forall Q,Q'\\in QuadraticMap(R,M,N): a \\cdot (Q+Q') = a \\cdot Q + a \\cdot Q',\\ a \\cdot 0 = 0,\\ (a b) \\cdot Q = a \\cdot (b \\cdot Q),\\ 1 \\cdot Q = Q.$$$
Lean4
instance [Monoid S] [DistribMulAction S N] [SMulCommClass S R N] : DistribMulAction S (QuadraticMap R M N)
where
mul_smul a b Q := ext fun x => by simp only [smul_apply, mul_smul]
one_smul Q := ext fun x => by simp only [QuadraticMap.smul_apply, one_smul]
smul_add a Q
Q' := by
ext
simp only [add_apply, smul_apply, smul_add]
smul_zero
a := by
ext
simp only [zero_apply, smul_apply, smul_zero]
