refactor(algebra/associated): rename nonzero_of_irreducible to ne_zero_of_irreducible

Author: ChrisHughes24

src/algebra/associated.lean

@@ -136,7 +136,7 @@ by simp [irreducible]
 | ⟨hn0, h⟩ := have is_unit (0:α) ∨ is_unit (0:α), from h 0 0 ((mul_zero 0).symm),
   this.elim hn0 hn0
 
-theorem nonzero_of_irreducible [semiring α] : ∀ {p:α}, irreducible p → p ≠ 0
+theorem ne_zero_of_irreducible [semiring α] : ∀ {p:α}, irreducible p → p ≠ 0
 | _ hp rfl := not_irreducible_zero hp
 
 theorem of_irreducible_mul {α} [monoid α] {x y : α} :

src/field_theory/splitting_field.lean

@@ -98,18 +98,18 @@ is_noetherian_ring.irreducible_induction_on (f.map i)
     by conv_lhs { rw eq_C_of_degree_eq_zero (is_unit_iff_degree_eq_zero.1 hu) };
       simp [leading_coeff, nat_degree_eq_of_degree_eq_some (is_unit_iff_degree_eq_zero.1 hu)]⟩)
   (λ f p hf0 hp ih hfs,
-    have hpf0 : p * f ≠ 0, from mul_ne_zero (nonzero_of_irreducible hp) hf0,
+    have hpf0 : p * f ≠ 0, from mul_ne_zero (ne_zero_of_irreducible hp) hf0,
     let ⟨s, hs⟩ := ih (splits_of_splits_mul _ hpf0 hfs).2 in
     ⟨-(p * norm_unit p).coeff 0 :: s,
       have hp1 : degree p = 1, from hfs.resolve_left hpf0 hp (by simp),
       begin
         rw [multiset.map_cons, multiset.prod_cons, leading_coeff_mul, C_mul, mul_assoc,
           mul_left_comm (C f.leading_coeff), ← hs, ← mul_assoc, domain.mul_right_inj hf0],
         conv_lhs {rw eq_X_add_C_of_degree_eq_one hp1},
-        simp only [mul_add, coe_norm_unit (nonzero_of_irreducible hp), mul_comm p, coeff_neg,
+        simp only [mul_add, coe_norm_unit (ne_zero_of_irreducible hp), mul_comm p, coeff_neg,
           C_neg, sub_eq_add_neg, neg_neg, coeff_C_mul, (mul_assoc _ _ _).symm, C_mul.symm,
           mul_inv_cancel (show p.leading_coeff ≠ 0, from mt leading_coeff_eq_zero.1
-            (nonzero_of_irreducible hp)), one_mul],
+            (ne_zero_of_irreducible hp)), one_mul],
       end⟩)
 
 section UFD

src/ring_theory/principal_ideal_domain.lean

@@ -127,7 +127,7 @@ lemma is_maximal_of_irreducible {p : α} (hp : irreducible p) :
 end⟩
 
 lemma irreducible_iff_prime {p : α} : irreducible p ↔ prime p :=
-⟨λ hp, (span_singleton_prime $ nonzero_of_irreducible hp).1 $
+⟨λ hp, (span_singleton_prime $ ne_zero_of_irreducible hp).1 $
     (is_maximal_of_irreducible hp).is_prime,
   irreducible_of_prime⟩
 

src/ring_theory/unique_factorization_domain.lean

@@ -70,8 +70,8 @@ multiset.induction_on (factors a)
               mt is_unit_of_mul_is_unit_left $ mt is_unit_of_mul_is_unit_left
                 (hs p (multiset.mem_cons_self _ _)).2.1),
     ⟨associated.symm (by clear _let_match; simp * at *), hs0 ▸ rfl⟩⟩)
-  (factors_prod (nonzero_of_irreducible ha))
-  (prime_factors (nonzero_of_irreducible ha))
+  (factors_prod (ne_zero_of_irreducible ha))
+  (prime_factors (ne_zero_of_irreducible ha))
 
 lemma irreducible_iff_prime {p : α} : irreducible p ↔ prime p :=
 by letI := classical.dec_eq α; exact
@@ -110,7 +110,7 @@ by haveI := classical.dec_eq α; exact
         (λ q (hq : q ∈ g.erase b), hg q (multiset.mem_of_mem_erase hq))
         (associated_mul_left_cancel
           (by rwa [← multiset.prod_cons, ← multiset.prod_cons, multiset.cons_erase hbg]) hb
-        (nonzero_of_irreducible (hf p (by simp)))))
+        (ne_zero_of_irreducible (hf p (by simp)))))
     end)
 
 end unique_factorization_domain
@@ -148,7 +148,7 @@ def of_unique_irreducible_factorization {α : Type*} [integral_domain α]
 by letI := classical.dec_eq α; exact
 { prime_factors := λ a h p (hpa : p ∈ o.factors a),
     have hpi : irreducible p, from o.irreducible_factors h _ hpa,
-    ⟨nonzero_of_irreducible hpi, hpi.1,
+    ⟨ne_zero_of_irreducible hpi, hpi.1,
       λ a b ⟨x, hx⟩,
       if hab0 : a * b = 0
       then (eq_zero_or_eq_zero_of_mul_eq_zero hab0).elim