prod_mapDomain_index_inj — Mathlib

English

For a CommMonoid N and f : α → β, s : α →₀ M, h : β → M → N, if f is injective, then (s.mapDomain f).prod h = s.prod (λ a b, h (f a) b).

Русский

Пусть N — комммоидный моноид, f : α → β, s : α →₀ M, h : β → M → N; если f инъективен, то (s.mapDomain f).prod h = s.prod (λ a b, h (f a) b).

LaTeX

$$$$ (s.mapDomain f).prod h = s.prod (\lambda a b, h (f a) b). $$$$

Lean4

@[to_additive]
theorem prod_mapDomain_index_inj [CommMonoid N] {f : α → β} {s : α →₀ M} {h : β → M → N} (hf : Function.Injective f) :
    (s.mapDomain f).prod h = s.prod fun a b => h (f a) b := by
  rw [← Function.Embedding.coeFn_mk f hf, ← embDomain_eq_mapDomain, prod_embDomain]

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