mathlib3
79349662 - Add the `normed_field` instance, rename `discrete` to `const`

Commit

3 years ago

Add the `normed_field` instance, rename `discrete` to `const`

References

#14621 - feat(topology,analysis): add the discrete metric and normed spaces

Author

eric-wieser

eric-wieser

Parents

Loading