mathlib

fbaa3ad0 - chore(linear_algebra/basic): add `linear_equiv.conj_apply_apply` (#17364)

chore(linear_algebra/basic): add `linear_equiv.conj_apply_apply` (#17364) While this lemma follows by `simp` via `conj_apply`, it is very annoying to clean up in a chain of rewrites due to having to commute all the coercions.