English
The tensor product A ⊗_R B is a semiring, with the usual left/right distributivity, zero properties, and multiplication axioms coming from mul and one_def.
Русский
Тензорное произведение A ⊗_R B образует полугруппу-кольцо с обычными распределениями и свойствами нуля/единицы.
LaTeX
$$$ \text{instSemiring} : \text{Semiring} (A \otimes_R B)$$$
Lean4
instance instSemiring : Semiring (A ⊗[R] B)
where
left_distrib a b c := by simp [HMul.hMul, Mul.mul]
right_distrib a b c := by simp [HMul.hMul, Mul.mul]
zero_mul a := by simp [HMul.hMul, Mul.mul]
mul_zero a := by simp [HMul.hMul, Mul.mul]
mul_assoc := Algebra.TensorProduct.mul_assoc
one_mul := Algebra.TensorProduct.one_mul
mul_one := Algebra.TensorProduct.mul_one
natCast_zero := AddMonoidWithOne.natCast_zero
natCast_succ := AddMonoidWithOne.natCast_succ
