cast_listProd

Mathlib.Data.NNRat.BigOperators

URI: https://scilib.ai/kg/mathlib#NNRat.cast_listProd

English

For any list l of nonnegative rationals, the cast of the product equals the product of the casts.

Русский

Для любого списка l из ℚ≥0, привод произведения равен произведению приводов элементов.

LaTeX

$$$(l.prod)^{\uparrow} = (l.map (\uparrow)).prod$$$

Lean4

@[norm_cast]
theorem cast_listProd (l : List ℚ≥0) : (l.prod : K) = (l.map (↑)).prod :=
  map_list_prod (castHom _) _

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

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

Разделы

Аффилиация

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