fst — Mathlib

English

The first projection fst from WithZero (G₀ˣ × H₀ˣ) to G₀ satisfies fst (g,h) = g.

Русский

Первая проекция fst с WithZero (G₀ˣ × H₀ˣ) на G₀ удовлетворяет fst (g,h) = g.

LaTeX

$$$fst\; (g,h) = g$$$

Lean4

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

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