snd — Mathlib

English

The inclusion inr: H₀ →*₀ WithZero (G₀ˣ × H₀ˣ) is defined similarly by mapping h to (1,g).

Русский

Включение inr: H₀ →*₀ WithZero (G₀ˣ × H₀ˣ) задаётся аналогично: h ↦ (1,h).

LaTeX

$$$\text{inr} : H_0 \to^*_0 WithZero (G_0^× × H_0^×)$$$

Lean4

/-- Given groups with zero `G₀`, `H₀`, the natural projection homomorphism from
`WithZero (G₀ˣ × H₀ˣ)` to `H₀`, which is the group with zero that can be identified
as their product. -/
def snd : WithZero (G₀ˣ × H₀ˣ) →*₀ H₀ :=
  WithZero.lift' ((Units.coeHom _).comp (.snd ..))

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