Commit 2026-04-20 07:57 4fceb469
View on Github →chore(LinearAlgebra/Dimension/StrongRankCondition): remove a redundant instance hypothesis (#38265)
The [Module.Finite R M] parameter is redundant and can be trivially removed.
I discovered this when investigating breakage in my project in #general > New simp lemma changes behavior on parameter omission. I don't think it is a direct cause of my problem, but while I am on it, I can make this trivial change.