Commit 2025-01-12 20:22 ea9d85f2

chore(Subalgebra/Unitization): move unrelated defs/lemmas earlier (#20526) The Subobject.toNonUnitalSubobject and NonUnitalSubobject.toSubobject functions (for Subobject = Subsemiring, Subring, Subalgebra, StarSubalgebra) were in Algebra.Algebra.Subalgebra.Unitization instead of where Subobject is defined. This PR moves them there, at the cost of importing NonUnitalSubobject when defining Subobject (which seems like a fine trade-off).