Commit 2024-11-28 14:24 0742f6cb

View on Github →

feat: interaction of Finset.sup and Nat.cast (#19245)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Ring/Finset.lean

added theorem Nat.cast_finsetInf'

added theorem Nat.cast_finsetSup'

added theorem Nat.cast_finsetSup

Modified Mathlib/Data/Nat/Cast/Order/Ring.lean

modified theorem Nat.cast_max

modified theorem Nat.cast_min