mathlib

646028a0 - refactor(data/finset/lattice): finset.{min,max} away from option (#15163)

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` Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>