English
For functions Q: ι → QuadraticMap R M N and finite set s, the application of the sum equals the sum of applications: (∑ i∈s Q(i)) (x) = ∑ i∈s Q(i)(x).
Русский
Для функций Q: ι → QuadraticMap и конечного множества s верно: (∑ i∈s Q(i)) (x) = ∑ i∈s Q(i)(x).
LaTeX
$$$\\big(\\sum_{i\\in s} Q(i)\\big)(x) = \\sum_{i\\in s} Q(i)(x).$$$
Lean4
/-- If `Q : M → N` is a quadratic map of `R`-modules and `R` is an `S`-algebra,
then the restriction of scalars is a quadratic map of `S`-modules. -/
@[simps!]
def restrictScalars (Q : QuadraticMap R M N) : QuadraticMap S M N
where
toFun x := Q x
toFun_smul a x := by simp [map_smul_of_tower]
exists_companion' :=
let ⟨B, h⟩ := Q.exists_companion
⟨B.restrictScalars₁₂ (S := R) (R' := S) (S' := S), fun x y => by
simp only [LinearMap.restrictScalars₁₂_apply_apply, h]⟩
