Theorem Algebra.Extension.Cotangent.mk_eq_zero_iff

Modification history

2025-01-09 15:53
Mathlib/RingTheory/Extension.lean
feat(RingTheory/StandardSmooth): pre-requisites for calculating the naive cotangent complex of a submersive presentation (#19749) …
Added Algebra.Extension.Cotangent.mk_eq_zero_iffView on Github →