rTensor_sub — Mathlib

English

For linear maps f,g: N → P, the right-tensor map distributes over subtraction: rTensor_Q (f - g) = rTensor_Q f - rTensor_Q g.

Русский

Правая тензорная карта распределяется по вычитанию: rTensor_Q (f - g) = rTensor_Q f - rTensor_Q g.

LaTeX

$$$$(f - g)_{\\rTensor Q} = f_{\\rTensor Q} - g_{\\rTensor Q}.$$$$

Lean4

@[simp]
theorem rTensor_sub (f g : N →ₗ[R] P) : (f - g).rTensor Q = f.rTensor Q - g.rTensor Q :=
  by
  simp only [← coe_rTensorHom]
  exact (rTensorHom (R := R) (N := N) (P := P) Q).map_sub f g

Похожие утверждения