tsum_div_const

Mathlib.Topology.Algebra.InfiniteSum.Ring

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

English

If the type supports division and is topologically compatible, ∑' i, f i / a = (∑' i, f i) / a.

Русский

Если имеется деление и совместимо с топологией, ∑' i, f(i)/a = (∑' i, f(i)) / a.

LaTeX

$$$[T2Space \alpha] \Rightarrow \sum' i, f(i) / a = (\sum' i, f(i)) / a$$$

Lean4

theorem tsum_div_const [T2Space α] : ∑'[L] x, f x / a = (∑'[L] x, f x) / a := by
  simpa only [div_eq_mul_inv] using tsum_mul_right

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

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

Разделы

Аффилиация

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