English
Given a bijection i from a subset of mulSupport g to β with certain compatibility, HasProd f a is equivalent to HasProd g a, provided f and g match along i and the supports align.
Русский
Если существует биекция i между подмножеством mulSupport g и β, удовлетворяющая совместимости, HasProd f a эквивалентно HasProd g a при условии согласованности функций along i.
LaTeX
$$$\exists i,\text{Injective}(i) \land (\text{superset conditions}) \land (\forall x, f(i(x)) = g(x)) \Rightarrow HasProd f a \iff HasProd g a$$$
Lean4
@[to_additive]
theorem hasProd_iff_hasProd_of_ne_one_bij {g : γ → α} (i : mulSupport g → β) (hi : Injective i)
(hf : mulSupport f ⊆ Set.range i) (hfg : ∀ x, f (i x) = g x) : HasProd f a ↔ HasProd g a :=
Iff.symm <|
Equiv.hasProd_iff_of_mulSupport
(Equiv.ofBijective (fun x ↦ ⟨i x, fun hx ↦ x.coe_prop <| hfg x ▸ hx⟩)
⟨fun _ _ h ↦ hi <| Subtype.ext_iff.1 h, fun y ↦ (hf y.coe_prop).imp fun _ hx ↦ Subtype.ext hx⟩)
hfg
