mathlib3
0d186304 - chore(ring_theory/norm): generalise a couple of lemmas (#15160)

Commit

3 years ago

chore(ring_theory/norm): generalise a couple of lemmas (#15160) Using the generalisation linter

Author

alexjbest

Parents