Theorems · Theorem · commutative algebra

Module.Invertible.exists_linearEquiv_ideal

∀ (R : Type u_5) (M : Type u_6) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.Invertible R M] [Subsingleton (CommRing.Pic (FractionRing R))], ∃ I, Nonempty (M ≃ₗ[R] ↥I)

If FractionRing R has trivial Picard group, every invertible R-module is isomorphic to an ideal.

Defined in

Mathlib.RingTheory.PicardGroup

Cited by

0 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleModule.InvertibleSubsingleton