Commit 2025-07-29 10:01 cd5e6a6e

View on Github →

fix(KaehlerDifferential): avoid brackets around Ω[S⁄R] notation (#27601) There is no reason to need the brackets around Ω[S⁄R]. This PR fixes the notation.

Estimated changes

Modified Mathlib/Algebra/Module/Presentation/Differentials.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean

Modified Mathlib/RingTheory/Extension/Cotangent/Basic.lean

Modified Mathlib/RingTheory/Kaehler/Basic.lean

modified def KaehlerDifferential.D

Modified Mathlib/RingTheory/Kaehler/Polynomial.lean

Modified Mathlib/RingTheory/Kaehler/TensorProduct.lean

Modified Mathlib/RingTheory/Smooth/Kaehler.lean

Modified Mathlib/RingTheory/Smooth/Local.lean

Modified Mathlib/RingTheory/Smooth/Locus.lean

Modified Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean

Modified Mathlib/RingTheory/Unramified/Basic.lean

Modified Mathlib/RingTheory/Unramified/Locus.lean