div

Mathlib.Topology.Algebra.InfiniteSum.Group

URI: https://scilib.ai/kg/mathlib#HasProd.div

← MathLib Explorer

English

If HasProd f a1 L and HasProd g a2 L, then HasProd (f/g) (a1/a2) L.

Русский

Если HasProd f a1 L и HasProd g a2 L, то HasProd (f/g) (a1/a2) L.

LaTeX

$$HasProd f a1 L → HasProd g a2 L → HasProd (fun b => f b / g b) (a1 / a2) L$$

Lean4

@[to_additive]
theorem div (hf : HasProd f a₁ L) (hg : HasProd g a₂ L) : HasProd (fun b ↦ f b / g b) (a₁ / a₂) L :=
  by
  simp only [div_eq_mul_inv]
  exact hf.mul hg.inv

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

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

Разделы

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

Аффилиация

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