Theorem RCLike.ofReal_eq_complex_ofReal

Modification history

2025-06-24 19:51

Mathlib/Analysis/Complex/Basic.lean

feat(Analysis/Complex): lemmas involving complex numbers and `IsSelfAdjoint` (#26034) …

Added RCLike.ofReal_eq_complex_ofReal View on Github →