trans_div

Mathlib.Topology.Algebra.InfiniteSum.Group

URI: https://scilib.ai/kg/mathlib#Multipliable.trans_div

← MathLib Explorer

English

If Multipliable g L and Multipliable (f/g) L, then Multipliable f L.

Русский

Если Multipliable g L и Multipliable (f/g) L, то Multipliable f L.

LaTeX

$$Multipliable g L → Multipliable (fun b => f b / g b) L → Multipliable f L$$

Lean4

@[to_additive]
theorem trans_div (hg : Multipliable g L) (hfg : Multipliable (fun b ↦ f b / g b) L) : Multipliable f L := by
  simpa only [div_mul_cancel] using hfg.mul hg

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

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

Разделы

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

Аффилиация

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