Commit 2024-04-18 05:39 df27bf71

View on Github →

chore(*): drop porting notes about List.nthLe → List.get (#12203)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/Combinatorics/Young/YoungDiagram.lean

modified def YoungDiagram.ofRowLens

Modified Mathlib/Data/List/Indexes.lean

Modified Mathlib/LinearAlgebra/Matrix/Transvection.lean

Modified Mathlib/Order/JordanHolder.lean