smul_aeeqFun_const — Mathlib

English

Smul of a constant function by aDMulAct element leaves the constant unchanged in AEEqFun.

Русский

Умножение константной функции на элемент действует тривиально на AEEqFun.

LaTeX

$$$c \\cdot (AEEqFun.const\\, \\alpha\\, b) = AEEqFun.const\\, \\alpha\\, b$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_aeeqFun_const (c : Mᵈᵐᵃ) (b : β) : c • (AEEqFun.const α b : α →ₘ[μ] β) = AEEqFun.const α b :=
  rfl

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