Commit 2021-01-27 08:41 688772e9

refactor(ring_theory/ideal ring_theory/jacobson): allow ideal in a comm_semiring (#5879) At the moment, ideal requires the underlying ring to be a comm_ring. This changes in this PR and the underlying ring can now be a comm_semiring. There is a discussion about merits and issues in this Zulip chat: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/(comm_)semiring.3A.20examples.3F At the moment, this PR changes the definition and adapts, mostly ring_theory/jacobson, to avoid deterministic timeouts. In future PRs, I will start changing hypotheses on lemmas involving ideal to use the more general framework. A note: the file ring_theory/jacobson might require further improvements. If possible, I would like this change to push through without cluttering it with changes to that file. If there is a way of accepting this change and then proceeding to the changes in jacobson, that would be ideal! If it needs to be done at the same time, then so be it!