tprod_eq_tprod_of_mulSupport — Mathlib

English

If an equivalence e between mulSupports exists and the coordinate-wise equality holds, then the tprod of f equals the tprod of g.

Русский

Если существует эквивалентность между mulSupports и выполняется попарное равенство координат, то т-произведение f равно т-произведению g.

LaTeX

$$$\\\\prod' x, f x = \\\\prod' y, g y$$$

Lean4

@[to_additive]
theorem tprod_eq_tprod_of_mulSupport {f : β → α} {g : γ → α} (e : mulSupport f ≃ mulSupport g)
    (he : ∀ x, g (e x) = f x) : ∏' x, f x = ∏' y, g y :=
  .symm <| tprod_eq_tprod_of_ne_one_bij _ (Subtype.val_injective.comp e.injective) (by simp) he

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