coe_snd — Mathlib

English

The underlying linear map of the second projection is the standard second projection map on the product.

Русский

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

LaTeX

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

Lean4

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

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