coe_fst — Mathlib

English

The underlying linear map of the first projection is the standard first projection map on the product, i.e., the linear part of fst is the product projection.

Русский

Непосредственно линейная часть первой проекции совпадает с обычной проекцией на первую координату в произведении.

LaTeX

$$$\uparrow(\mathrm{fst}\ R\ M_1\ M_2) = \mathrm{LinearMap.fst}\ R\ M_1\ M_2.$$$

Lean4

@[simp, norm_cast]
theorem coe_fst : ↑(fst R M₁ M₂) = LinearMap.fst R M₁ M₂ :=
  rfl

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