Theorems · Theorem · commutative algebra

Module.Projective.out

∀ {R : Type u_1} {inst : Semiring R} {P : Type u_2} {inst_1 : AddCommMonoid P} {inst_2 : Module R P}
  [self : Module.Projective R P], ∃ s, Function.LeftInverse ⇑(Finsupp.linearCombination R id) ⇑s

Defined in

Mathlib.Algebra.Module.Projective

Cited by

2 results in Mathlib

Foundations

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

Assumes

Module.Projective