HepLean Documentation

Mathlib.RingTheory.Finiteness.Projective

Finite and projective modules #

theorem Module.Finite.exists_comp_eq_id_of_projective (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Module.Projective R M] :
∃ (n : ) (f : (Fin nR) →ₗ[R] M) (g : M →ₗ[R] Fin nR), Function.Surjective f Function.Injective g f ∘ₗ g = LinearMap.id