extend_smul — Mathlib

English

For M acting on β and with f: ι → α, g: ι → β, e: α → β, we have extend f (r • g) (r • e) = r • extend f g e for r∈M. The smul commutes with the extend operation.

Русский

Пусть M действует на β, f: ι → α, g: ι → β, e: α → β. Тогда extend f (r•g) (r•e) = r•extend f g e для любого r∈M; действие линейно взаимно с операцией extend.

LaTeX

$$$Extend\;f\; (r\cdot g)\; (r\cdot e) = r\cdot\Extend\;f\; g\; e.$$$

Lean4

@[to_additive]
theorem extend_smul {M α β : Type*} [SMul M β] (r : M) (f : ι → α) (g : ι → β) (e : α → β) :
    extend f (r • g) (r • e) = r • extend f g e := by
  funext x
  classical
  simp only [extend_def, Pi.smul_apply]
  split_ifs <;> rfl

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