leanprover-community / mathlib

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.66k stars 297 forks source link

[Merged by Bors] - chore(ring_theory/kaehler): cleanup instances #19234

Closed eric-wieser closed 11 months ago

eric-wieser commented 12 months ago

The previous module instance has the wrong defeqs, and was more work to construct. The new one remains propositionally equal to the old one.


Open in Gitpod

riccardobrasca commented 11 months ago

Thanks!

bors merge

bors[bot] commented 11 months ago

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.