Commit 2021-10-11 07:59 4a191ad9

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.