Theorem IsROrC.conj_tsum

Modification history

2024-03-28 10:26

Mathlib/Analysis/Complex/Basic.lean

chore: Rename `IsROrC` to `RCLike` (#10819) …

Deleted IsROrC.conj_tsum View on Github →

2023-05-15 21:28

Mathlib/Analysis/Complex/Basic.lean

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

Added IsROrC.conj_tsum View on Github →