Commit 2026-06-02 10:39 8a1ec5f2
View on Github →chore(RingTheory/PicardGroup): drop StrongRankCondition assumptions in two lemmas (#39231)
The StrongRankCondition was demanded by Module.finrank_self but can be obtained directly from commutativity via CommSemiring.finrank_self.