Theorem RCLike.ofReal_lt_ofReal

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_lt_ofRealView on Github →