mathlib
1605b859 - feat(data/real/ennreal): add ennreal.to_(nn)real_inv and ennreal.to_(nn)real_div (#9144)

Commit
4 years ago
feat(data/real/ennreal): add ennreal.to_(nn)real_inv and ennreal.to_(nn)real_div (#9144)
Author
Parents
Loading