Theorem Ideal.range_cotangentToQuotientSquare

Modification history

2025-01-08 16:06
Mathlib/RingTheory/Ideal/Cotangent.lean
feat(RingTheory/Smooth): calculate `H¹(L)` via formally smooth extensions (#20471)
Added Ideal.range_cotangentToQuotientSquareView on Github →