English
Unitization(R, A) forms a non-associative semiring under the defined addition and multiplication.
Русский
Unitization(R, A) образует полугруппу с неассоциативным умножением и сложением.
LaTeX
$$$\text{Unitization}(R,A) \text{ is a NonAssocSemiring.}$$$
Lean4
instance instNonAssocSemiring [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] :
NonAssocSemiring (Unitization R A) :=
{ Unitization.instMulOneClass,
Unitization.instAddCommMonoid with
zero_mul := fun x =>
ext (zero_mul x.1) <|
show (0 : R) • x.2 + x.1 • (0 : A) + 0 * x.2 = 0 by rw [zero_smul, zero_add, smul_zero, zero_mul, add_zero]
mul_zero := fun x =>
ext (mul_zero x.1) <|
show x.1 • (0 : A) + (0 : R) • x.2 + x.2 * 0 = 0 by rw [smul_zero, zero_add, zero_smul, mul_zero, add_zero]
left_distrib := fun x₁ x₂ x₃ =>
ext (mul_add x₁.1 x₂.1 x₃.1) <|
show
x₁.1 • (x₂.2 + x₃.2) + (x₂.1 + x₃.1) • x₁.2 + x₁.2 * (x₂.2 + x₃.2) =
x₁.1 • x₂.2 + x₂.1 • x₁.2 + x₁.2 * x₂.2 + (x₁.1 • x₃.2 + x₃.1 • x₁.2 + x₁.2 * x₃.2)
by
simp only [smul_add, add_smul, mul_add]
abel
right_distrib := fun x₁ x₂ x₃ =>
ext (add_mul x₁.1 x₂.1 x₃.1) <|
show
(x₁.1 + x₂.1) • x₃.2 + x₃.1 • (x₁.2 + x₂.2) + (x₁.2 + x₂.2) * x₃.2 =
x₁.1 • x₃.2 + x₃.1 • x₁.2 + x₁.2 * x₃.2 + (x₂.1 • x₃.2 + x₃.1 • x₂.2 + x₂.2 * x₃.2)
by
simp only [add_smul, smul_add, add_mul]
abel }
