mathlib3

73f96237 - chore(ring_theory/kaehler): extract from `ring_theory/derivation` (#18935)

chore(ring_theory/kaehler): extract from `ring_theory/derivation` (#18935) This section of the file needs heavier imports than the first half; and this splits the content nicely in two. The lemmas are moved without modification. One very minor docstring typo is fixed.