mathlib
caa58cbf
- chore(data/{complex,is_R_or_C}/basic): fix name of `eq_conj_iff_*` lemmas (#18922)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
2 years ago
chore(data/{complex,is_R_or_C}/basic): fix name of `eq_conj_iff_*` lemmas (#18922) These were all about `conj x = x` not `x = conj x`.
Author
eric-wieser
Parents
15e02bcd
Loading