smul_eq — Mathlib

English

If HasSum f s, HasSum g t, and HasSum of the double product equals u, then s • t = u.

Русский

Если HasSum f s, HasSum g t, и HasSum от двойного произведения равна u, тогда s • t = u.

LaTeX

$$$$ \text{HasSum } f s \to \text{HasSum } g t \to \text{HasSum } (f\_1 \cdot g\_1) u \Rightarrow s \cdot t = u. $$$$

Lean4

theorem smul_eq (hf : HasSum f s) (hg : HasSum g t) (hfg : HasSum (fun x : ι × κ ↦ f x.1 • g x.2) u) : s • t = u :=
  have key₁ : HasSum (fun i ↦ f i • t) (s • t) := hf.smul_const t
  have this : ∀ i : ι, HasSum (fun c : κ ↦ f i • g c) (f i • t) := fun i ↦ hg.const_smul (f i)
  have key₂ : HasSum (fun i ↦ f i • t) u := HasSum.prod_fiberwise hfg this
  key₁.unique key₂

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