Def Complex.ofRealClm

Modification history

2024-01-26 03:03

Mathlib/Analysis/Complex/Basic.lean

fix: `Clm` -> `CLM`, `Cle` -> `CLE` (#10018) …

Deleted Complex.ofRealClm View on Github →

2023-05-15 21:28

Mathlib/Analysis/Complex/Basic.lean

feat: port Analysis.Complex.Basic (#3930)

Added Complex.ofRealClm View on Github →