Mathlib Changelog
v4
Changelog
About
Github
Theorem
RCLike.ofReal_pos
Modification history
2024-06-12 11:07
Mathlib/Analysis/RCLike/Basic.lean
feat: generalize `Matrix.PosDef.det_pos` to complex matrices (#13744) …
Added
RCLike.ofReal_pos
View on Github →