mathlib
6b408eb1 - feat(data/real/nnreal): define `nnreal.gi : galois_insertion of_real coe` (#1699)

Commit
6 years ago
feat(data/real/nnreal): define `nnreal.gi : galois_insertion of_real coe` (#1699)
Author
Committer
Parents
Loading