snd — Mathlib

English

Similarly, the second projection is an M-equivariant map.

Русский

Аналогично, вторая проекция является M-эквивариантным отображением.

LaTeX

$$$\textsnd:\alpha\times\beta \to[M]\beta\text{ is }M\text{-equivariant.}$$$

Lean4

/-- `Prod.snd` as a bundled `MulActionHom`. -/
@[to_additive (attr := simps -fullyApplied) /-- `Prod.snd` as a bundled `AddActionHom`. -/
    ]
def snd : α × β →[M] β where
  toFun := Prod.snd
  map_smul' _ _ := rfl

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