Commit 2026-10-10 13:11 20090887

View on Github →

feat(LinearAlgebra): make two Nontrivial theorems low priority instances (#44558) Turn nontrivial_of_invariantBasisNumber and nontrivial_of_hasRankNullity into low priority instances. I think the original intention of them being theorems was to avoid TC slowdowns, but the performance impact appears to be relatively contained.

Estimated changes

Modified Mathlib/Algebra/Module/SpanRank.lean

Modified Mathlib/Algebra/QuadraticAlgebra/IsQuadraticExtension.lean

Modified Mathlib/LinearAlgebra/Charpoly/Basic.lean

Modified Mathlib/LinearAlgebra/Dimension/Constructions.lean

modified theorem Pi.dim_spanSubset

modified theorem finrank_span_eq_card

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

Modified Mathlib/LinearAlgebra/Dimension/Free.lean

Modified Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean

Modified Mathlib/LinearAlgebra/Dimension/LinearMap.lean

Modified Mathlib/LinearAlgebra/Dimension/RankNullity.lean

modified theorem nontrivial_of_hasRankNullity

Modified Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

Modified Mathlib/LinearAlgebra/InvariantBasisNumber.lean

modified theorem nontrivial_of_invariantBasisNumber

Modified Mathlib/LinearAlgebra/Matrix/Rank.lean

modified theorem Matrix.cRank_one

modified theorem Matrix.eRank_one

Modified Mathlib/RingTheory/Trace/Basic.lean