Theorem KaehlerDifferential.exact_mapBaseChange_map

Modification history

2024-04-29 06:31
Mathlib/RingTheory/Kaehler.lean
feat(RingTheory/Kaehler): The exact sequence `B ⊗[A] Ω[A⁄R] → Ω[B⁄R] → Ω[B⁄A] → 0`. (#11925)
Added KaehlerDifferential.exact_mapBaseChange_mapView on Github →