Commit 2025-12-18 10:09 32e3f3ff

View on Github →

chore(LinearAlgebra): fix whitespace (#32952) Extracted from https://github.com/leanprover-community/mathlib4/pull/30658. Found by extending the commandStart linter to proof bodies.

Estimated changes

modified theorem right_lt_lineMap_iff_one_lt
modified theorem SModEq.neg
modified theorem SpecialLinearGroup.coe_div
modified theorem SpecialLinearGroup.coe_mul