mathlib3
fdabe9c3 - feat(data/padics/padic_norm): add a little more API (#5082)

Commit
5 years ago
feat(data/padics/padic_norm): add a little more API (#5082) A little more API for `padic_val_rat` and `padic_val_nat`.
Author
Parents
Loading