mathlib3

0dabcb8e - chore(ring_theory/ideal/operations): relax the base ring of algebras from comm_ring to comm_semiring (#10024)

chore(ring_theory/ideal/operations): relax the base ring of algebras from comm_ring to comm_semiring (#10024) This also tidies up some variables and consistently uses `B` instead of `S` for the second algebra. One proof in `ring_theory/finiteness.lean` has to be redone because typeclass search times out where it previously did not. Thankfully, the new proof is shorter anyway.