feat(algebra/algebra/unitization): define unitization of a non-unital…

… algebra (#12601)

Given a non-unital `R`-algebra `A` (given via the type classes `[non_unital_ring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A]`) we construct the minimal unital `R`-algebra containing `A` as an ideal. This object `unitization R A` is a type synonym for `R × A` on which we place a different multiplicative structure, namely, `(r₁, a₁) * (r₂, a₂) = (r₁ * r₂, r₁ • a₂ + r₂ • a₁ + a₁ * a₂)` where the multiplicative identity is `(1, 0)`.