multipliable_iff_of_multipliable_div

Mathlib.Topology.Algebra.InfiniteSum.Group

URI: https://scilib.ai/kg/mathlib#multipliable_iff_of_multipliable_div

← MathLib Explorer

English

If HasProd f x, then HasProd (norm f) (norm x).

Русский

Если HasProd f x, то HasProd (норма f) (норма x).

LaTeX

$$HasProd f x → HasProd (norm ∘ f) (norm x)$$

Lean4

@[to_additive]
theorem multipliable_iff_of_multipliable_div (hfg : Multipliable (fun b ↦ f b / g b) L) :
    Multipliable f L ↔ Multipliable g L :=
  ⟨fun hf ↦ hf.trans_div <| by simpa only [inv_div] using hfg.inv, fun hg ↦ hg.trans_div hfg⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru