Commit 2022-02-07 10:17 3c70566a

feat(analysis/normed_space/linear_isometry): symm_trans (#11892) Add a simp lemma linear_isometry_equiv.symm_trans, like coe_symm_trans but without a coercion involved. coe_symm_trans can then be proved by simp, so stops being a simp lemma itself.