prod_one — Mathlib

English

The right unit acts as the identity for the pointwise product with any filter l on α: l ×ˢ (1 : Filter α) = map (·, 1) l.

Русский

Правая единица служит тождеством для точечного произведения: l ×ˢ (1 : Filter α) = map (·, 1) l.

LaTeX

$$$l \\timesˢ (1 : Filter \\alpha) = \\mathrm{map}(\\cdot, 1)\, l$$$

Lean4

@[to_additive (attr := simp) prod_zero]
theorem prod_one {l : Filter β} : l ×ˢ (1 : Filter α) = map (·, 1) l :=
  prod_pure

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