Commit 2023-05-16 18:39 46235134

View on Github →

chore: forward-port mathlib#18554 (#3982) Match [#18554](https://github.com/leanprover-community/mathlib/pull/18554)

Estimated changes

Modified Mathlib/Algebra/Order/LatticeGroup.lean

added def LatticeOrderedAddCommGroup.IsSolid

added theorem LatticeOrderedAddCommGroup.isSolid_solidClosure

added def LatticeOrderedAddCommGroup.solidClosure

added theorem LatticeOrderedAddCommGroup.solidClosure_min

Modified Mathlib/Analysis/Normed/Order/Lattice.lean

added theorem LatticeOrderedAddCommGroup.isSolid_ball

added theorem norm_le_norm_of_abs_le_abs

deleted theorem solid