Commit 2024-09-25 02:09 3c4370ef

View on Github →

fix: do not rely on the definition for List.ofFn (#17118)

Estimated changes

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean

modified theorem WeierstrassCurve.Projective.smul_fin3

Modified Mathlib/Combinatorics/Optimization/ValuedCSP.lean

Modified Mathlib/Computability/Primrec.lean

Modified Mathlib/LinearAlgebra/CrossProduct.lean

Modified Mathlib/LinearAlgebra/Dimension/RankNullity.lean

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

modified theorem ExteriorAlgebra.ιMulti_zero_apply

Modified Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean