English
The structure tsze_R M carries a nonassociative semiring structure.
Русский
Структура tsze_R M образует неассоциированное полупрямое полуполугруппу и т.д.
LaTeX
$$$\text{NonAssocSemiring}(\mathrm{tsze}_{R} M)$$$
Lean4
instance nonAssocSemiring [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] : NonAssocSemiring (tsze R M) :=
{ TrivSqZeroExt.addMonoidWithOne, TrivSqZeroExt.mulOneClass,
TrivSqZeroExt.addCommMonoid with
zero_mul := fun x =>
ext (zero_mul x.1) <| show (0 : R) •> x.2 + (0 : M) <• x.1 = 0 by rw [zero_smul, zero_add, smul_zero]
mul_zero := fun x =>
ext (mul_zero x.1) <| show x.1 • (0 : M) + (0 : Rᵐᵒᵖ) • x.2 = 0 by rw [smul_zero, zero_add, zero_smul]
left_distrib := fun x₁ x₂ x₃ =>
ext (mul_add x₁.1 x₂.1 x₃.1) <|
show x₁.1 •> (x₂.2 + x₃.2) + x₁.2 <• (x₂.1 + x₃.1) = x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)
by simp_rw [smul_add, MulOpposite.op_add, add_smul, add_add_add_comm]
right_distrib := fun x₁ x₂ x₃ =>
ext (add_mul x₁.1 x₂.1 x₃.1) <|
show (x₁.1 + x₂.1) •> x₃.2 + (x₁.2 + x₂.2) <• x₃.1 = x₁.1 •> x₃.2 + x₁.2 <• x₃.1 + (x₂.1 •> x₃.2 + x₂.2 <• x₃.1)
by simp_rw [add_smul, smul_add, add_add_add_comm] }