Theorem KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap

Modification history

2025-01-20 11:48
Mathlib/RingTheory/Etale/Kaehler.lean
feat(RingTheory): `H¹(L)` under localization (#20591)
Added KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMapView on Github →