Theorems · Theorem · commutative algebra

Module.free_of_isStablyFree_of_invertible

∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.IsStablyFree R M] [Module.Invertible R M], Module.Free R M

Let R be a commutative ring, M be a finite stably free R-module. Then M is free if it is invertible.

Defined in

Mathlib.Algebra.Module.StablyFree.FreeOfInvertible

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleModule.IsStablyFreeModule.Invertible