prod_pi_mulSingle'

Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

URI: https://scilib.ai/kg/mathlib#Fintype.prod_pi_mulSingle'

← MathLib Explorer

English

A variant: ∏ j, Pi.mulSingle i a j = a.

Русский

Вариант: ∏_{j} Pi.mulSingle i a j = a.

LaTeX

$$$\\displaystyle \\prod_{j} \\Pi.mulSingle i a j = a$$$

Lean4

/-- See also `Finset.prod_pi_mulSingle'`. -/
@[to_additive /-- See also `Finset.sum_pi_single'`. -/
    ]
theorem prod_pi_mulSingle' (i : ι) (a : M) : ∏ j, Pi.mulSingle i a j = a :=
  prod_dite_eq' _ _

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

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

Разделы

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

Аффилиация

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