mathlib3
2c2338e7 - chore(data/complex/basic): add of_real_eq_one (#11496)

Commit

3 years ago

chore(data/complex/basic): add of_real_eq_one (#11496)

Author

eric-wieser

eric-wieser

Parents

Loading