English
For f : Finsupp α M and g : α → M → Real, the embedding commutes with finsupp products: (RCLike.ofReal (f.prod (λ a b, g a b))) = f.prod (λ a b, RCLike.ofReal (g a b)).
Русский
Для f : Finsupp α M и g : α → M → Real отображение сохраняет finsuppProduct: RCLike.ofReal (f.prod ...) = f.prod (RCLike.ofReal ...).
LaTeX
$$$\;\; {K}\text{ } {\alpha} \text{ } {M} \; [Zero\ M]
(f : Finsupp \alpha M) (g : \alpha \to M \to \mathrm{Real})\;:
((f.prod fun a b => g a b) : K) = f.prod fun a b => RCLike.ofReal (g a b)$$$
Lean4
@[simp, rclike_simps, norm_cast]
theorem ofReal_finsuppProd {α M : Type*} [Zero M] (f : α →₀ M) (g : α → M → ℝ) :
((f.prod fun a b => g a b : ℝ) : K) = f.prod fun a b => (g a b : K) :=
map_finsuppProd _ f g
