Skip to content

Commit

Permalink
chore(ring_theory/kaehler): extract from ring_theory/derivation (#1…
Browse files Browse the repository at this point in the history 
…8935)

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.
  • Loading branch information
@eric-wieser
eric-wieser committed May 3, 2023
1 parent 92c69b7 commit 73f9623
Show file tree
Hide file tree
Showing 3 changed files with 642 additions and 623 deletions.

0 comments on commit 73f9623

Please sign in to comment.