Commit 2020-06-28 08:10 2f6a5f59
View on Github →feat(nat, lattice): preliminaries for Haar measure (#3190)
PR 2/5 to put the Haar measure in mathlib. This PR: results about lattices and lattice operations on nat
.
add some simp lemmas for nat.find
(simplifying a proof in sum_four_squares
)
rename finset.sup_val
to finset.sup_def
(it was unused). In PR 3 I will add a new declaration finset.sup_val
Inf_nat_def
and Sup_nat_def
renamed to nat.Inf_def
and nat.Sup_def
, and use set.nonempty
in statement (they were unused outside that file)