Commit 2026-01-21 17:08 83a8be66

refactor: @[simp] for e.conj f x = e (f (e.symm x)) (#34183) This came up while reviewing PR #33615. Not only LinearMap & LinearEquiv but also other bundled maps often simplify when applied. So it's natural to have a simp lemma for e.conj f x. This simp lemma has lower priority, because it should rewrite after unapplied conj lemmas for performance reason (e.g. e.conj LinearMap.id x => LinearMap.id x => x rather than e.conj LinearMap.id x => e (LinearMap.id (e.symm x)) => e (e.symm x) => x)