Theorem Module.Invertible.finrank_eq_one

Modification history

2025-11-04 08:07
Mathlib/RingTheory/PicardGroup.lean
feat(RingTheory): finite flat constant rank module over semilocal ring is free (#31241) …
Deleted Module.Invertible.finrank_eq_oneView on Github →
2025-08-16 08:07
Mathlib/RingTheory/PicardGroup.lean
feat(RingTheory): invertible modules and Picard group (#25337)
Added Module.Invertible.finrank_eq_oneView on Github →