tprod_eq_one_of_not_multipliable

Mathlib.Topology.Algebra.InfiniteSum.Defs

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

English

For any injective g, HasProd f a (L.map g) is equivalent to HasProd (f ∘ g) a L.

Русский

Для инъективного g: HasProd f a (L.map g) эквивалентно HasProd (f ∘ g) a L.

LaTeX

$$$ HasProd f a (L.map ⟨g, hg⟩) \leftrightarrow HasProd (f \circ g) a L $$$

Lean4

@[to_additive]
theorem tprod_eq_one_of_not_multipliable (h : ¬Multipliable f L) : ∏'[L] b, f b = 1 := by simp [tprod_def, h]

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

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

Разделы

Аффилиация

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