Skip to content

Commit 4fceb46

Browse files
committed
chore(LinearAlgebra/Dimension/StrongRankCondition): remove a redundant instance hypothesis (leanprover-community#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](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/New.20simp.20lemma.20changes.20behavior.20on.20parameter.20omission/with/586399020). I don't think it is a direct cause of my problem, but while I am on it, I can make this trivial change.
1 parent 40de301 commit 4fceb46

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -531,7 +531,7 @@ theorem finrank_eq_zero_iff_of_free [Module.Free R M] [Module.Finite R M] :
531531
simp [Module.finrank, this, Module.rank_zero_iff_of_free]
532532

533533
@[simp]
534-
theorem finrank_eq_zero_of_subsingleton [Module.Free R M] [Module.Finite R M] [Subsingleton M] :
534+
theorem finrank_eq_zero_of_subsingleton [Module.Free R M] [Subsingleton M] :
535535
Module.finrank R M = 0 :=
536536
(finrank_eq_zero_iff_of_free R M).mpr inferInstance
537537

0 commit comments

Comments
 (0)