hasProd_one — Mathlib

English

The constant-one function has product 1 with respect to any summation filter L.

Русский

Постоянно единичная функция имеет произведение, равное единице, по отношению к любому фильтру суммирования L.

LaTeX

$$$HasProd (\\lambda _ \\to 1) 1 L$$$

Lean4

/-- Constant one function has product `1` -/
@[to_additive /-- Constant zero function has sum `0` -/
    ]
theorem hasProd_one : HasProd (fun _ ↦ 1 : β → α) 1 L := by simp [HasProd, tendsto_const_nhds]

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