Commit 2024-02-04 23:05 3646044d

View on Github →

chore(LinearAlgebra,BigOperators): drop some decidability assumptions (#10237) Found by a linter from #10235.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Ring.lean

Modified Mathlib/LinearAlgebra/DFinsupp.lean

modified theorem DFinsupp.sum_mapRange_index.linearMap

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

modified theorem Matrix.PosSemidef.dotProduct_mulVec_zero_iff

modified theorem Matrix.posSemidef_iff_eq_transpose_mul_self

Modified Mathlib/LinearAlgebra/Matrix/Spectrum.lean

modified theorem Matrix.IsHermitian.exists_eigenvector_of_ne_zero

Modified Mathlib/Tactic/NormNum/BigOperators.lean

modified theorem Mathlib.Meta.Multiset.insert_eq_cons