mathlib
a1107a4e - Eliminate `finish` from `normed_lattice_add_comm_group`

Commit

4 years ago

Eliminate `finish` from `normed_lattice_add_comm_group`

Author

stuart-presnell

stuart-presnell

Parents

Loading