Commit 2023-08-04 08:48 d32630e8

feat: maps between the unitization of a non-unital subalgebra and its Algebra.adjoin (#5602) If S is non-unital subalgebra of a unital R-algebra A, there is a natural surjective map Unitization R S →ₐ[R] Algebra.adjoin R (S : Set A). When 1 ∉ S and R is a field, this becomes and AlgEquiv. We specialize this to the ℕ-unitization of a non-unital subsemiring and its Subsemiring.closure, as well as the ℤ-unitization of a non-unital subring and its Subring.closure. We also extend the above map to a StarAlgHom in the case of NonUnitalStarSubalgebras. This continues the non-unital-ization of mathlib.

• depends on: #5151
• depends on: #5512
• depends on: #5537