Theorem Module.Invertible.rank_eq_one

Modification history

2025-08-16 08:07

Mathlib/RingTheory/PicardGroup.lean

feat(RingTheory): invertible modules and Picard group (#25337)

Added Module.Invertible.rank_eq_one View on Github →