one_smul — Mathlib

English

The unit scalar from the external ring acts as the identity on the tensor product: 1 · x = x for all x ∈ M ⊗_R N.

Русский

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

LaTeX

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

Lean4

protected theorem one_smul (x : M ⊗[R] N) : (1 : R') • x = x :=
  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, one_smul]) fun x y ihx ihy => by
    rw [TensorProduct.smul_add, ihx, ihy]

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