inrNonUnitalAlgHom — Mathlib

English

inrNonUnitalAlgHom maps A into Unitization(R,A) as a nonunital algebra homomorphism.

Русский

inrNonUnitalAlgHom отображает A в Unitization(R,A) как немонолитный алгебра-гомоморфизм.

LaTeX

$$$A \to_{R} Unitization(R,A)\ a \mapsto inr(a)$$$

Lean4

/-- The coercion from a non-unital `R`-algebra `A` to its unitization `Unitization R A`
realized as a non-unital algebra homomorphism. -/
@[simps]
def inrNonUnitalAlgHom (R A : Type*) [CommSemiring R] [NonUnitalSemiring A] [Module R A] : A →ₙₐ[R] Unitization R A
    where
  toFun := (↑)
  map_smul' := inr_smul R
  map_zero' := inr_zero R
  map_add' := inr_add R
  map_mul' := inr_mul R

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