Commit 2025-11-10 15:24 32fb6832

feat(RingTheory/Extension/Cotangent): presentation is submersive if I/I² has a suitable basis (#28769) Let P be a presentation of an algebra with kernel I. We show that if I/I² has a basis given by the images of the relations and the module of Kaehler differentials has a basis given by the differentials of the free generators (those that don't appear in the Jacobian matrix), then P is submersive. We will later deduce from this a presentation-independent characterization of standard smooth algebras. From Pi1.