mathlib
8c60a927 - fix(ring_theory/algebraic): prove a diamond exists and remove the instances (#11935)

Commit

4 years ago

fix(ring_theory/algebraic): prove a diamond exists and remove the instances (#11935) It seems nothing used these instances anyway.

Author

eric-wieser

Parents