Mathlib v3 is deprecated. Go to Mathlib v4

Def complex.conj

Modification history

2021-10-21 23:04

src/data/complex/basic.lean

refactor(data/complex/*): replace `complex.conj` and `is_R_or_C.conj` with star (#9640) …

Deleted complex.conj View on Github →

2020-07-01 17:12

src/data/complex/basic.lean

chore(*): work on removing deprecated is_X_hom typeclasses (#3258) …

Modified complex.conj View on Github →

2018-01-20 17:03

data/complex.lean

refactor(data/complex): clean up proofs

Added complex.conj View on Github →