Revision #1498 → #1785 · back to history
modifiedProjective is free over a PID (Quillen–Suslin)e9a628ec082d
| Field | From #1498 | To #1785 |
|---|
| mathlib.decl | Submodule.exists_basis_of_pid | Submodule.basisOfPid |
| moderation_flag | — | Label mentions Quillen–Suslin but that theorem is about polynomial rings, not PIDs in general; the underlying mathematical claim here (projective over PID is free) is correct. |
| note | Mathlib proves submodules of free modules over a PID are free, but not the full 'every projective is free over a PID' as one declaration. | Mathlib proves submodules of free modules over a PID are free (Submodule.basisOfPid), but not the full 'every projective is free over a PID' as one declaration. |
| provenance | ai | ai-moderated |
modifiedProjective abelian groups are free0c9a690b79e5
| Field | From #1498 | To #1785 |
|---|
| mathlib.decl | Submodule.exists_basis_of_pid | Submodule.basisOfPid |
| note | PID infrastructure gives the result for finite-type ℤ-modules, but the general 'projective abelian group is free' iff is not a single declaration. | PID infrastructure (Submodule.basisOfPid) gives the result for finite-type ℤ-modules, but the general 'projective abelian group is free' iff is not a single declaration. |