mathlib

4a191ad9 - feat(algebra.algebra.subalgebra): add `subalgebra.gc_map_comap` (#9435)

feat(algebra.algebra.subalgebra): add `subalgebra.gc_map_comap` (#9435) Other changes: * add `linear_map.coe_inl`/`linear_map.coe_inr` and move `@[simp]` from `inl_apply`/`inr_apply` to these lemmas; * fix a typo in the name (`adjoint` → `adjoin`); * drop `algebra.adjoin_inl_union_inr_le_prod `: we prove an equality anyway; * add `alg_hom.map_adjoin` (same as `(adjoin_image _ _ _).symm`) to match `monoid_hom.map_closure` etc.