feat(algebra/ne_zero): add helper methods (#14286)

Also golfs the inspiration for one of these, and cleans up some code around the area.
leanprover-community · May 23, 2022 · 275dd0f · 275dd0f
1 parent 15f49ae
commit 275dd0f
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 7 deletions.
diff --git a/src/algebra/ne_zero.lean b/src/algebra/ne_zero.lean
@@ -47,23 +47,26 @@ instance char_zero [ne_zero n] [add_monoid M] [has_one M] [char_zero M] : ne_zer
 @[priority 100] instance invertible [mul_zero_one_class M] [nontrivial M] [invertible x] :
   ne_zero x := ⟨nonzero_of_invertible x⟩
 
-instance coe_trans {r : R} [has_zero M] [has_coe R S] [has_coe_t S M] [h : ne_zero (r : M)] :
+instance coe_trans [has_zero M] [has_coe R S] [has_coe_t S M] [h : ne_zero (r : M)] :
   ne_zero ((r : S) : M) := ⟨h.out⟩
 
-lemma trans {r : R} [has_zero M] [has_coe R S] [has_coe_t S M] (h : ne_zero ((r : S) : M)) :
+lemma trans [has_zero M] [has_coe R S] [has_coe_t S M] (h : ne_zero ((r : S) : M)) :
   ne_zero (r : M) := ⟨h.out⟩
 
 lemma of_map [has_zero R] [has_zero M] [zero_hom_class F R M] (f : F) [ne_zero (f r)] :
   ne_zero r := ⟨λ h, ne (f r) $ by convert map_zero f⟩
 
-lemma of_injective {r : R} [has_zero R] [h : ne_zero r] [has_zero M] [zero_hom_class F R M]
+lemma of_injective [has_zero R] [h : ne_zero r] [has_zero M] [zero_hom_class F R M]
   {f : F} (hf : function.injective f) : ne_zero (f r) :=
 ⟨by { rw ←map_zero f, exact hf.ne (ne r) }⟩
 
 lemma nat_of_injective [non_assoc_semiring M] [non_assoc_semiring R] [h : ne_zero (n : R)]
   [ring_hom_class F R M] {f : F} (hf : function.injective f) : ne_zero (n : M) :=
  ⟨λ h, (ne_zero.ne' n R) $ hf $ by simpa⟩
 
+lemma pos (r : R) [canonically_ordered_add_monoid R] [ne_zero r] : 0 < r :=
+(zero_le r).lt_of_ne $ ne_zero.out.symm
+
 variables (R M)
 
 lemma of_not_dvd [add_monoid M] [has_one M] [char_p M p] (h : ¬ p ∣ n) : ne_zero (n : M) :=
@@ -84,3 +87,6 @@ lemma pos_of_ne_zero_coe [has_zero R] [has_one R] [has_add R] [ne_zero (n : R)]
 (ne_zero.of_ne_zero_coe R).out.bot_lt
 
 end ne_zero
+
+lemma eq_zero_or_ne_zero {α} [has_zero α] (a : α) : a = 0 ∨ ne_zero a :=
+(eq_or_ne a 0).imp_right ne_zero.mk
diff --git a/src/data/zmod/basic.lean b/src/data/zmod/basic.lean
@@ -79,19 +79,19 @@ def zmod : ℕ → Type
 namespace zmod
 
 instance fintype : Π (n : ℕ) [fact (0 < n)], fintype (zmod n)
-| 0     h := false.elim $ nat.not_lt_zero 0 h.1
+| 0     h := (lt_irrefl _ h.1).elim
 | (n+1) _ := fin.fintype (n+1)
 
-instance fintype' (n : ℕ) [hn : ne_zero n] : fintype (zmod n) :=
-@zmod.fintype n ⟨nat.pos_of_ne_zero hn.1⟩
+instance fintype' (n : ℕ) [ne_zero n] : fintype (zmod n) :=
+@zmod.fintype n ⟨ne_zero.pos n⟩
 
 instance infinite : infinite (zmod 0) :=
 int.infinite
 
 @[simp] lemma card (n : ℕ) [fintype (zmod n)] : fintype.card (zmod n) = n :=
 begin
   casesI n,
-  { exfalso, exact not_fintype (zmod 0) },
+  { exact (not_fintype (zmod 0)).elim },
   { convert fintype.card_fin (n+1) }
 end