Mathlib v3 is deprecated. Go to Mathlib v4

Def lattice_ordered_add_comm_group.solid_closure

Modification history

2023-05-11 05:57
src/algebra/order/lattice_group.lean
feat(analysis/normed/order/lattice): add has_solid_norm (#18554) …
Added lattice_ordered_add_comm_group.solid_closureView on Github →