Mathlib Changelog
v4
Changelog
About
Github
Theorem
Ideal.to_quotient_square_range
Modification history
2025-01-08 16:06
Mathlib/RingTheory/Ideal/Cotangent.lean
feat(RingTheory/Smooth): calculate `H¹(L)` via formally smooth extensions (#20471)
Deleted
Ideal.to_quotient_square_range
View on Github →
2023-05-29 12:31
Mathlib/RingTheory/Ideal/Cotangent.lean
feat: port RingTheory.Ideal.Cotangent (#4451)
Added
Ideal.to_quotient_square_range
View on Github →