Commit 2026-05-23 11:09 34599470

View on Github →

chore: IsBotZeroClass (Fin n) (#39058) We also deprecate a bunch of theorems that now follow from the typeclass.

Estimated changes

Modified Archive/Imo/Imo2024Q5.lean

Modified Mathlib/AlgebraicTopology/Quasicategory/Basic.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean

Modified Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean

Modified Mathlib/Combinatorics/Additive/FreimanHom.lean

Modified Mathlib/Data/Fin/SuccPred.lean

Modified Mathlib/GroupTheory/Perm/Sign.lean

Modified Mathlib/Logic/Equiv/Fin/Rotate.lean

Modified Mathlib/Order/Fin/Basic.lean

deleted theorem Fin.bot_eq_zero

Modified Mathlib/Order/Grade.lean

Modified Mathlib/Order/Interval/Set/Basic.lean

added theorem Set.Iio_one_eq_empty

Modified Mathlib/RingTheory/ChainOfDivisors.lean