Commit 2025-05-01 01:14 e052dad2

View on Github →

feat(Fin/Basic): add 2 simp attrs and a simp lemma (#24196)

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.castSucc_ne_last

modified theorem Fin.predAbove_last_castSucc

modified theorem Fin.predAbove_zero_succ

modified theorem Fin.succ_succAbove_zero

Modified Mathlib/Data/Fin/Tuple/Basic.lean

Modified Mathlib/GroupTheory/Perm/Fin.lean

Modified Mathlib/LinearAlgebra/Basis/Flag.lean

Modified Mathlib/LinearAlgebra/InvariantBasisNumber.lean

Modified Mathlib/Order/JordanHolder.lean

Modified Mathlib/RingTheory/Idempotents.lean

Modified Mathlib/RingTheory/NoetherNormalization.lean

Modified MathlibTest/matrix.lean