prod_map_one

Mathlib.Algebra.BigOperators.Group.Multiset.Defs

URI: https://scilib.ai/kg/mathlib#Multiset.prod_map_one

English

The product of mapping every element to 1 is 1: prod (m.map (λ _, 1)) = 1.

Русский

Произведение отображения каждого элемента в единицу равно единице: prod (m.map (λ _, 1)) = 1.

LaTeX

$$$\\mathrm{prod}(\\mathrm{map}(\\lambda\\_ , 1)\\ m) = 1$$$

Lean4

@[to_additive]
theorem prod_map_one : prod (m.map fun _ => (1 : M)) = 1 := by rw [map_const', prod_replicate, one_pow]

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

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

Разделы

Аффилиация

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