Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-08 00:21 646028a0

View on Github →

refactor(data/finset/lattice): finset.{min,max} away from option (#15163) Switch to a with_top/with_bot based API. This avoids exposing option as implementation detail. Redefines polynomial.degree to use coe instead of some

Estimated changes

modified theorem finset.le_max'
modified theorem finset.le_max_of_mem
modified theorem finset.max_empty
added theorem finset.max_eq_bot
deleted theorem finset.max_eq_none
modified theorem finset.max_of_mem
modified theorem finset.max_of_nonempty
modified theorem finset.max_singleton
modified theorem finset.mem_of_max
modified theorem finset.mem_of_min
modified theorem finset.min'_le
modified theorem finset.min_empty
deleted theorem finset.min_eq_none
added theorem finset.min_eq_top
modified theorem finset.min_le_of_mem
modified theorem finset.min_of_mem
modified theorem finset.min_of_nonempty
modified theorem finset.min_singleton
modified def polynomial.degree
added def with_bot.unbot'
added theorem with_bot.unbot'_bot
added theorem with_bot.unbot'_coe
added def with_top.untop'
added theorem with_top.untop'_coe
added theorem with_top.untop'_top