multipliable_iff_of_hasProd_iff — Mathlib

English

Let e be a surjective map and suppose HasProd f (e a) ↔ HasProd g a for all a. Then Multipliable f ↔ Multipliable g.

Русский

Пусть e — сюръективное отображение и для всех a выполнено HasProd f (e a) ↔ HasProd g a. Тогда Multipliable f ↔ Multipliable g.

LaTeX

$$Multipliable f ↔ Multipliable g$$

Lean4

@[to_additive]
theorem multipliable_iff_of_hasProd_iff {α' : Type*} [CommMonoid α'] [TopologicalSpace α'] {e : α' → α}
    (hes : Function.Surjective e) {f : β → α} {g : γ → α'} (he : ∀ {a}, HasProd f (e a) ↔ HasProd g a) :
    Multipliable f ↔ Multipliable g :=
  hes.exists.trans <| exists_congr <| @he

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