Commit 2026-11-10 21:24 02970ca0

View on Github →

chore(LinearAlgebra): remove unused hypothesis (#45690) Removes unused hypothesis from #45673 in LinearAlgebra.

Estimated changes

Modified Mathlib/Algebra/Lie/Weights/Killing.lean

Modified Mathlib/Analysis/Convex/Between.lean

Modified Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

modified theorem affineSpan_image_ne_top_of_encard_le_finrank

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

deleted theorem affineIndepOn_of_ne

added theorem affineIndepOn_pair

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

Modified Mathlib/LinearAlgebra/Lagrange.lean

modified theorem Lagrange.eval_interpolate_not_at_node'

Modified Mathlib/LinearAlgebra/Projectivization/PSL/PSL2.lean

Modified Mathlib/LinearAlgebra/Projectivization/PSL/Stabilizer.lean

Modified Mathlib/LinearAlgebra/RootSystem/Reduced.lean

deleted theorem RootPairing.pairing_neg_one_neg_four_iff'

deleted theorem RootPairing.pairing_one_four_iff'