Commit 2022-03-29 23:24 50903f0d

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).