Def Algebra.Extension.tensorCotangentSpace

Modification history

2026-03-17 15:35
Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean
feat(RingTheory): `Extension.CotangentSpace` commutes with base change (#35594) …
Added Algebra.Extension.tensorCotangentSpaceView on Github →
2026-03-02 12:12
Mathlib/RingTheory/Etale/Kaehler.lean
chore(RingTheory/Etale/Kaehler): mention `FormallyEtale` in the names (#35699) …
Deleted Algebra.Extension.tensorCotangentSpaceView on Github →
2025-01-20 11:48
Mathlib/RingTheory/Etale/Kaehler.lean
feat(RingTheory): `H¹(L)` under localization (#20591)
Added Algebra.Extension.tensorCotangentSpaceView on Github →