English
If S → R is an algebra and R,a,b defined, then QuadraticAlgebra R a b carries a natural algebra structure over S.
Русский
Если имеется алгебраическая связь S→R и задано R,a,b, то над S естественно существует структура S-алгебры на QuadraticAlgebra R a b.
LaTeX
$$$Algebra\ S\bigl(\QuadraticAlgebra R a b\bigr)$$$
Lean4
instance [CommSemiring S] [CommSemiring R] [Algebra S R] : Algebra S (QuadraticAlgebra R a b)
where
algebraMap.toFun s := coe (algebraMap S R s)
algebraMap.map_one' := by ext <;> simp
algebraMap.map_mul' x y := by ext <;> simp
algebraMap.map_zero' := by ext <;> simp
algebraMap.map_add' x y := by ext <;> simp
commutes' s z := by ext <;> simp [Algebra.commutes]
smul_def' s x := by ext <;> simp [Algebra.smul_def]
