Theorem IsROrC.ofReal_mul_re

Modification history

2024-01-09 21:58
Mathlib/Data/IsROrC/Basic.lean
feat: Basic `Complex` lemmas (#9527) …
Deleted IsROrC.ofReal_mul_reView on Github →
2023-05-12 05:54
Mathlib/Data/IsROrC/Basic.lean
feat: port Data.IsROrC.Basic (#3654)
Added IsROrC.ofReal_mul_reView on Github →