Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.re_eq_add_conj

Modification history

2018-01-21 23:57

data/complex.lean

feat(data/real): real square root function, sqrt 2 is irrational

Added complex.re_eq_add_conj View on Github →