Skip to content

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

Closed
SnirBroshi wants to merge 1 commit into
leanprover-community:masterfrom
SnirBroshi:feature/matrix/det-eq-zero-of-mulvec-nonzerodivisor
Closed

[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:masterfrom
SnirBroshi:feature/matrix/det-eq-zero-of-mulvec-nonzerodivisor

Commits

Commits on May 21, 2026