Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-03-01 16:22
7f82eb86
View on Github →
feat(Data/Fin): add
@[simp]
lemmas (
#22259
)
Estimated changes
Modified
Archive/Imo/Imo2024Q5.lean
Modified
Mathlib/Algebra/BigOperators/Fin.lean
Modified
Mathlib/Algebra/Group/Fin/Basic.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
Modified
Mathlib/Combinatorics/Enumerative/Composition.lean
Modified
Mathlib/Data/Fin/Basic.lean
deleted
theorem
Fin.castSucc_pos'
added
theorem
Fin.castSucc_pos_iff
added
theorem
Fin.mk_eq_one
added
theorem
Fin.mk_eq_zero
added
theorem
Fin.one_eq_mk
added
theorem
Fin.val_eq_zero_iff
added
theorem
Fin.val_ne_zero_iff
added
theorem
Fin.val_pos_iff
deleted
theorem
Fin.val_zero'
added
theorem
Fin.zero_eq_mk
Modified
Mathlib/LinearAlgebra/Matrix/Circulant.lean
Modified
Mathlib/RingTheory/ChainOfDivisors.lean