mathlib
a5a7a753 - feat(analysis/normed_space): define `normed_comm_ring` (#4291)

Commit

5 years ago

feat(analysis/normed_space): define `normed_comm_ring` (#4291) Also use section `variables`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

References

#4925 - Make prime-avoidance branch build

Author

urkud

Parents

9962bfa7

mathlib a5a7a753 - feat(analysis/normed_space): define `normed_comm_ring` (#4291)

mathlib
a5a7a753 - feat(analysis/normed_space): define `normed_comm_ring` (#4291)