Commit 2020-07-01 23:16 93099107

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_)rings/division_rings/fields. 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_zeros and domains;
• 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;