mathlib

688772e9 - refactor(ring_theory/ideal ring_theory/jacobson): allow `ideal` in a `comm_semiring` (#5879)

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!