prod_map_one

Mathlib.Algebra.BigOperators.Group.List.Defs

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

Lean4

@[to_additive]
theorem prod_map_one {l : List ι} : (l.map fun _ => (1 : M)).prod = 1 := by
  induction l with
  | nil => rfl
  | cons hd tl ih => rw [map_cons, prod_one_cons, ih]

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

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

Разделы

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

Аффилиация

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