Commit 2022-03-03 16:19 c5045853
View on Github →fix(number_theory/number_field): make ring_of_integers_algebra not an instance (#12331) This issue has caused problems for at least two of Kevin's PhD students; it is better to remove it for now or disable it temporarily. c.f. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/diamond.20for.20monoid.20instance.20on.20ideals