mathlib

ac2addd1 - feat(linear_algebra): lemmas on associatedness of determinants of linear maps (#15587)

feat(linear_algebra): lemmas on associatedness of determinants of linear maps (#15587) `det f` equals `det f'` up to units if `f'` is `f` composed with a linear equiv. First a homogeneous form where `f f' : M → M`, then a heterogeneous form where `f f' : M → N` and the equivs `e e' : N → M`. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>