mathlib

93099107 - chore(algebra/*): deduplicate `*_with_zero`/`semiring`/`field` (#3259)

chore(algebra/*): deduplicate `*_with_zero`/`semiring`/`field` (#3259) All moved/renamed/merged lemmas were generalized to use `*_with_zero`/`nonzero`/`mul_zero_class` instead of `(semi)ring`/`division_ring`/`field`. ## Moved to `group_with_zero` The following lemmas were formulated for `(semi_)ring`s/`division_ring`s/`field`s. Some of them had strictly more general “prime” versions for `*_with_zero`. I either moved a lemma to `algebra/group_with_zero` and adjusted the requirements or removed the non-prime version and `'` from the name of the prime version. Sometimes I also made some arguments implicit. TL;DR: moved to `group_with_zero`, removed `name'` lemma if it was there. * `is_unit_zero_iff`; * `not_is_unit_zero`; * `div_eq_one_iff_eq`; * `eq_div_iff_mul_eq`; * `eq_div_of_mul_eq`; * `eq_one_div_of_mul_eq_one`; * `eq_one_div_of_mul_eq_one_left`; * `one_div_one_div`; * `eq_of_one_div_eq_one_div`; * `one_div_div`; * `mul_eq_of_eq_div`; * `mul_mul_div`; * `eq_zero_of_zero_eq_one`; * `eq_inv_of_mul_right_eq_one`; * `eq_inv_of_mul_left_eq_one`; * `div_right_comm`; * `div_div_div_cancel_right`; * `div_mul_div_cancel`; ## Renamed/merged * rename `mul_inv''` to `mul_inv'` and merge `mul_inv'` into `mul_inv_rev'`; * `coe_unit_mul_inv`, `coe_unit_inv_mul`: `units.mul_inv'`, `units.inv_mul'` * `division_ring.inv_eq_iff`: `inv_eq_iff`; * `division_ring.inv_inj`: `inv_inj'`; * `domain.mul_left_inj`: `mul_left_inj'`; * `domain.mul_right_inj`: `mul_right_inj'`; * `eq_of_mul_eq_mul_of_nonzero_left` and `eq_of_mul_eq_mul_left`: `mul_left_cancel'`; * `eq_of_mul_eq_mul_of_nonzero_right` and `eq_of_mul_eq_mul_right`: `mul_right_cancel'`; * `inv_inj`, `inv_inj'`, `inv_inj''`: `inv_injective`, `inv_inj`, and `inv_inj'`, respectively; * `mul_inv_cancel_assoc_left`, `mul_inv_cancel_assoc_right`, `inv_mul_cancel_assoc_left`, `inv_mul_cancel_assoc_right`: `mul_inv_cancel_left'`, `mul_inv_cacnel_right'`, `inv_mul_cancel_left'`, `inv_mul_cancel_right'`; * `ne_zero_and_ne_zero_of_mul_ne_zero` : `ne_zero_and_ne_zero_of_mul`. * `ne_zero_of_mul_left_eq_one`: `left_ne_zero_of_mul_eq_one` * `ne_zero_of_mul_ne_zero_left` : `right_ne_zero_of_mul`; * `ne_zero_of_mul_ne_zero_right` : `left_ne_zero_of_mul`; * `ne_zero_of_mul_right_eq_one`: `left_ne_zero_of_mul_eq_one` * `neg_inj` and `neg_inj` renamed to `neg_injective` and `neg_inj`; * `one_inv_eq`: merged into `inv_one`; * `unit_ne_zero`: `units.ne_zero`; * `units.mul_inv'` and `units.inv_mul'`: `units.mul_inv_of_eq` and `units.inv_mul_of_eq`; * `units.mul_left_eq_zero_iff_eq_zero`, `units.mul_right_eq_zero_iff_eq_zero`: `units.mul_left_eq_zero`, `units.mul_right_eq_zero`; ## New * `class cancel_monoid_with_zero`: a `monoid_with_zero` such that left/right multiplication by a non-zero element is injective; the main instances are `group_with_zero`s and `domain`s; * `monoid_hom.map_ne_zero`, `monoid_hom.map_eq_zero`, `monoid_hom.map_inv'`, `monoid_hom.map_div`, `monoid_hom.injective`: lemmas about monoid homomorphisms of two groups with zeros such that `f 0 = 0`; * `mul_eq_zero_of_left`, `mul_eq_zero_of_right`, `ne_zero_of_eq_one` * `unique_of_zero_eq_one`, `eq_of_zero_eq_one`, `nonzero_psum_unique`, `zero_ne_one_or_forall_eq_0`; * `mul_left_inj'`, `mul_right_inj'` ## Misc changes * `eq_of_div_eq_one` no more requires `b ≠ 0`;