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

Closed

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

eric-wieser wants to merge 2 commits into master from eric-wieser/golf-kaehler

chore(ring_theory/kaehler): cleanup instances

317d3213

fix

7e3fdf1f

eric-wieser added awaiting-review

github-actions added modifies-synchronized-file

eric-wieser added t-algebra

eric-wieser added not-too-late

riccardobrasca assigned

riccardobrasca 2 years ago

github-actions added ready-to-merge

github-actions removed awaiting-review

bors changed the title ~~chore(ring_theory/kaehler): cleanup instances~~ [Merged by Bors] - chore(ring_theory/kaehler): cleanup instances 2 years ago

bors closed this 2 years ago

bors deleted the eric-wieser/golf-kaehler branch 2 years ago

Reviewers

No reviews

Assignees

riccardobrasca

Labels

ready-to-merge t-algebra modifies-synchronized-file not-too-late

Milestone

No milestone

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

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

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

Closed