mathlib
8ac7e3ba - feat(topology/instances/nnreal): add `nnreal.pow_order_iso` (#16344)

Commit
3 years ago
feat(topology/instances/nnreal): add `nnreal.pow_order_iso` (#16344) Also use it to redefine `nnreal.sqrt`.
Author
Parents
Loading