Theorem KaehlerDifferential.ideal_fg

Modification history

2024-07-15 20:56

Mathlib/RingTheory/Kaehler/Basic.lean

feat(RingTheory/Unramified): Unramified + free => finite (#14478)

Added KaehlerDifferential.ideal_fg View on Github →