instModule — Mathlib

English

Let S be a Semiring and R an AddCommMonoid with an S-Module structure on R. Then QuadraticAlgebra R a b is an S-Module, with add_smul and zero_smul laws.

Русский

Пусть S — полупривод, R — абелева группа по сложению, на которой действует структура модуля над S. Тогда QuadraticAlgebra R a b образует S-модуль, удовлетворяющий правилам add_smul и zero_smul.

LaTeX

$$$Module S (QuadraticAlgebra R a b)$$$

Lean4

instance [Semiring S] [AddCommMonoid R] [Module S R] : Module S (QuadraticAlgebra R a b)
    where
  add_smul r s x := by ext <;> simp [add_smul]
  zero_smul x := by ext <;> simp

Похожие утверждения