English
Tensor product distributes over subtraction in the second component: m1 - m2 tensored with n equals m1⊗n - m2⊗n.
Русский
Тензорное произведение распределяет вычитание по второму компоненту: (m1 - m2) ⊗ n = m1 ⊗ n - m2 ⊗ n.
LaTeX
$$$$(m_1 - m_2) \\otimes_R n = m_1 \\otimes_R n - m_2 \\otimes_R n.$$$$
Lean4
instance addCommGroup : AddCommGroup (M ⊗[R] N) :=
{ TensorProduct.addCommMonoid with
neg := Neg.neg
sub := _
sub_eq_add_neg := fun _ _ => rfl
neg_add_cancel := fun x => TensorProduct.neg_add_cancel x
zsmul := fun n v => n • v
zsmul_zero' := by simp
zsmul_succ' := by simp [add_comm, TensorProduct.add_smul]
zsmul_neg' := fun n x => by
change (-n.succ : ℤ) • x = -(((n : ℤ) + 1) • x)
rw [← zero_add (_ • x), ← TensorProduct.neg_add_cancel ((n.succ : ℤ) • x), add_assoc, ← add_smul, ←
sub_eq_add_neg, sub_self, zero_smul, add_zero]
rfl }
