notation. [ca-0017]
notation. [ca-0017]
Following literatures, for \(r \in R\),
usually we write \(\mathit {1}_A(r) : R \to _{+*} A\) as a product \(r \mathit {1}_A\) if not omitted,
while they are written as a call to
algebraMap _ _ r in \(\textsf {Mathlib}\),
which is defined to be Algebra.toRingHom r.