instRingHomSurjectiveProdSnd — Mathlib

English

The underlying function of the RingHom snd equals Prod.snd; i.e., snd is the standard second-coordinate projection morphism.

Русский

Базовая функция snd равна стандартной проекции на вторую координату.

LaTeX

$$$\\text{coe}_{\\text{snd}}: \\text{snd } R S = \\pi_2,$ where $\\pi_2$ is the second projection.$$

Lean4

instance (R S) [Semiring R] [Semiring S] : RingHomSurjective (snd R S) :=
  ⟨(⟨⟨0, ·⟩, rfl⟩)⟩

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