Theorem Module.Invertible.rank_eq_one

Modification history

2026-06-02 10:39
Mathlib/RingTheory/PicardGroup.lean
chore(RingTheory/PicardGroup): drop `StrongRankCondition` assumptions in two lemmas (#39231) …
Modified Module.Invertible.rank_eq_oneView on Github →
2025-08-16 08:07
Mathlib/RingTheory/PicardGroup.lean
feat(RingTheory): invertible modules and Picard group (#25337)
Added Module.Invertible.rank_eq_oneView on Github →