Theorem Module.Flat.of_linearEquiv

Modification history

2025-01-17 07:37

Mathlib/RingTheory/Flat/Basic.lean

feat(RingTheory): flatness over a semiring (#19115) …

Modified Module.Flat.of_linearEquiv View on Github →

2023-10-31 10:54

Mathlib/RingTheory/Flat.lean

feat(RingTheory/Flat): free and projective modules over a `CommRing` are flat (#7567) …

Added Module.Flat.of_linearEquiv View on Github →