fstHom — Mathlib

English

fstHom preserves unit and multiplication on Unitization.

Русский

fstHom сохраняет единицу и умножение в Unitization.

LaTeX

$$$\mathrm{fstHom}(1) = 1_R$, $\mathrm{fstHom}(x\cdot y) = \mathrm{fstHom}(x)\cdot \mathrm{fstHom}(y)$$$

Lean4

/-- The canonical `R`-algebra projection `Unitization R A → R`. -/
@[simps]
def fstHom : Unitization R A →ₐ[R] R where
  toFun := fst
  map_one' := fst_one
  map_mul' := fst_mul
  map_zero' := fst_zero (A := A)
  map_add' := fst_add
  commutes' := fst_inl A

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