Commit 2023-05-03 01:24 9c999503

View on Github →

feat port: Algebra.FreeModule.Determinant (#3767)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/FreeModule/Determinant.lean

added theorem LinearMap.det_zero''