English
In a non-unital non-associative algebra, multiplication is bilinear: it is linear in each argument separately over R.
Русский
В неедоставляющей единой единицы и неассоциативной алгебре умножение би-линейно: линейно по каждому аргументу отдельно над R.
LaTeX
$$$$ mul: A \times A \to A \quad\text{is bilinear over } R, \text{ i.e. }
\begin{cases} (a_1+a_2) b = a_1 b + a_2 b,\ a(b_1+b_2)= ab_1+ ab_2,\ (r a)b = r (ab),\ a(rb) = r (ab). \end{cases}$$$$
Lean4
/-- The multiplication in a non-unital non-associative algebra is a bilinear map.
A weaker version of this for semirings exists as `AddMonoidHom.mul`. -/
@[simps!]
def mul : A →ₗ[R] A →ₗ[R] A :=
LinearMap.mk₂ R (· * ·) add_mul smul_mul_assoc mul_add mul_smul_comm
