Commit 2024-06-12 11:07 1660695a

View on Github →

feat: generalize Matrix.PosDef.det_pos to complex matrices (#13744) Also adds some missing norm_cast lemmas

Estimated changes

Modified Mathlib/Analysis/RCLike/Basic.lean

added theorem RCLike.ofReal_lt_ofReal

added theorem RCLike.ofReal_lt_zero

added theorem RCLike.ofReal_pos

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

modified theorem Matrix.PosDef.det_pos