Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-04 16:45 5df2e7bb

View on Github →

chore(data/polynomial, data/finset/lattice): basic lemmas (#11237)

Estimated changes

Modified src/data/finset/lattice.lean

added theorem finset.coe_inf_of_nonempty

added theorem finset.coe_sup_of_nonempty

Modified src/data/polynomial/degree/definitions.lean

added theorem polynomial.degree_mono