English
Under suitable assumptions, Unitization(R, A) carries a multiplicative identity 1 and satisfies left and right identity laws: 1 · x = x and x · 1 = x.
Русский
При заданных предпосылках Unitization(R, A) имеет единицу умножения 1, которая удовлетворяет 1 · x = x и x · 1 = x.
LaTeX
$$$\forall x \in Unitization(R,A),\ 1 \cdot x = x = x \cdot 1.$$$
Lean4
instance instMulOneClass [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] :
MulOneClass (Unitization R A) :=
{ Unitization.instOne,
Unitization.instMul with
one_mul := fun x =>
ext (one_mul x.1) <|
show (1 : R) • x.2 + x.1 • (0 : A) + 0 * x.2 = x.2 by rw [one_smul, smul_zero, add_zero, zero_mul, add_zero]
mul_one := fun x =>
ext (mul_one x.1) <|
show (x.1 • (0 : A)) + (1 : R) • x.2 + x.2 * (0 : A) = x.2 by
rw [smul_zero, zero_add, one_smul, mul_zero, add_zero] }
