Commit 2024-12-13 08:43 2d8f64e7

View on Github →

feat: generalize LinearMap.det_smul (#19885)

Estimated changes

Modified Mathlib/LinearAlgebra/Determinant.lean

modified theorem LinearMap.det_smul

modified theorem LinearMap.det_zero

Modified Mathlib/LinearAlgebra/FreeModule/Determinant.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

modified theorem MeasureTheory.det_one_smulRight