[Merged by Bors] - feat(LinearAlgebra/Matrix/Adjugate): M.det = 0 if M *ᵥ v = 0 where v contains a non-zero-divisor#39642

SnirBroshi wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

SnirBroshi:feature/matrix/det-eq-zero-of-mulvec-nonzerodivisorSnirBroshi/mathlib4:feature/matrix/det-eq-zero-of-mulvec-nonzerodivisorCopy head branch name to clipboard