Theorems · Theorem · commutative algebra

Module.IsStablyFree.of_free_prod

∀ (R : Type u) [inst : Ring R] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Type w)
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.Finite R N] [Module.Free R N] [Module.Free R (M × N)],
  Module.IsStablyFree R M

Defined in

Mathlib.Algebra.Module.StablyFree.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleAddCommGroupModuleModule.FiniteModule.FreeModule.Free