Commit 2023-04-23 09:27 9d2364ad

View on Github →

feat: port LinearAlgebra.Matrix.AbsoluteValue (#3597)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/AbsoluteValue.lean

added theorem Matrix.det_le

added theorem Matrix.det_sum_le

added theorem Matrix.det_sum_smul_le