Commit 2024-04-10 12:08 9b4cab57

View on Github →

chore(RingTheory/Unramified): move differential properties (#12030)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Etale/Basic.lean

Modified Mathlib/RingTheory/Unramified/Basic.lean

deleted theorem Algebra.FormallyUnramified.iff_subsingleton_kaehlerDifferential

Created Mathlib/RingTheory/Unramified/Derivations.lean

added theorem Algebra.FormallyUnramified.iff_subsingleton_kaehlerDifferential