single_smul — Mathlib

English

For any a,b and f, and any r in a monoid with zero action, single a r b • f a = single a (r • f b) b, i.e., smul distributes through the singleton.

Русский

Для любых a,b и f, и любого r из моноида с нулём, выполняется equality: single a r b • f a = single a (r • f b) b.

LaTeX

$$$\\mathrm{single}(a, r) \\cdot f(a) = \\mathrm{single}(a, r \\cdot f(b))$$$

Lean4

@[simp]
theorem single_smul (a b : α) (f : α → M) (r : R) : single a r b • f a = single a (r • f b) b := by
  by_cases h : a = b <;> simp [h]

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