Stable freeness interface for projective modules

This module records the application-independent right-module formulation of stable freeness used in filtered-ring arguments. It is a definition, not a claim that any particular ring has the property.

def AlgebraicAnalysis.StablyFree.StablyFreeProjectives (R : Type u) [Ring R] : Prop

Every finitely generated projective right R-module becomes finite free after adding a finite free summand. Right modules are represented as modules over Rᵐᵒᵖ, so the order of scalar multiplication remains explicit.

Equations

• One or more equations did not get rendered due to their size.