zero_smul — Mathlib

English

The zero scalar from the external ring acts trivially on the tensor product: 0 · x = 0 for all x ∈ M ⊗_R N.

Русский

Нулевой скаляр из внешнего кольца действует тривиально на тензорном произведении: 0 · x = 0 для всех x ∈ M ⊗_R N.

LaTeX

$$$0 \cdot x = 0 \quad \text{for all } x \in M \otimes_R N$$$

Lean4

protected theorem zero_smul (x : M ⊗[R] N) : (0 : R'') • x = 0 :=
  have : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ n := fun _ _ _ => rfl
  x.induction_on (by rw [TensorProduct.smul_zero]) (fun m n => by rw [this, zero_smul, zero_tmul]) fun x y ihx ihy => by
    rw [TensorProduct.smul_add, ihx, ihy, add_zero]

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