smul_single_one — Mathlib

English

In a MulZeroOneClass, scaling the basis δ_a by b sends δ_a 1 to δ_a b, i.e., b • single a 1 = single a b.

Русский

В классе MulZeroOne, масштабирование базиса δ_a на b даёт δ_a b: b • single a 1 = single a b.

LaTeX

$$$[MulZeroOneClass R] \\ (a : \\alpha) \\; (b : R) : b \\cdot \\mathrm{single}(a,1) = \\mathrm{single}(a,b)$$$

Lean4

theorem smul_single_one [MulZeroOneClass R] (a : α) (b : R) : b • single a (1 : R) = single a b := by
  rw [smul_single, smul_eq_mul, mul_one]

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