multipliable_iff_of_mulSupport — Mathlib

English

Let e be an equivalence of the underlying elements of mulSupport for f and g; if a compatibility condition holds, then HasProd f a ↔ HasProd g a.

Русский

Пусть e — эквивалент между элементами mulSupport f и mulSupport g; при выполнении совместимости, HasProd f a ↔ HasProd g a.

LaTeX

$$$e:\; (\operatorname{mulSupport} f).\Elem \simeq (\operatorname{mulSupport} g).\Elem \Rightarrow HasProd f a \iff HasProd g a$$$

Lean4

@[to_additive]
theorem multipliable_iff_of_mulSupport {g : γ → α} (e : mulSupport f ≃ mulSupport g)
    (he : ∀ x : mulSupport f, g (e x) = f x) : Multipliable f ↔ Multipliable g :=
  exists_congr fun _ ↦ e.hasProd_iff_of_mulSupport he

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