Commit 2022-05-04 00:13 fc3de197

feat(ring_theory/ideal/local_ring): generalize lemmas to semirings (#13471) What is essentially new is the proof of local_ring.of_surjective and local_ring.is_unit_or_is_unit_of_is_unit_add.

• I changed the definition of local ring to local_ring.of_is_unit_or_is_unit_of_add_one, which is reminiscent of the definition before the recent change in #13341. The equivalence of the previous definition is essentially given by local_ring.is_unit_or_is_unit_of_is_unit_add. The choice of the definition is insignificant here because they are all equivalent, but I think the choice here is better for the default constructor because this condition is "weaker" than e.g. local_ring.of_non_units_add in some sense.
• The proof of local_ring.of_surjective needs [is_local_ring_hom f], which was not necessary for commutative rings in the previous proof. So the new version here is not a genuine generalization of the previous version. The previous version was renamed to local_ring.of_surjective'.