Theorem Module.Invertible.bijective_curry

Modification history

2025-08-16 08:07

Mathlib/RingTheory/PicardGroup.lean

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

Added Module.Invertible.bijective_curry View on Github →