feat(algebra/char_p): use finite instead of fintype (#16002)

* rename `char_ne_zero_of_fintype` to `char_ne_zero_of_finite`, use `[finite _]`;
* rename `ring_char_ne_zero_of_fintype` to `ring_char_ne_zero_of_finite`, use `[finite _]`;
* split `is_unit_iff_not_dvd_char_of_ring_char_ne_zero` from the proof of `is_unit_iff_not_dvd_char`;
* add aliases `is_coprime.nat_coprime` and `nat.coprime.is_coprime`.

Author: urkud

src/algebra/char_p/basic.lean

@@ -349,13 +349,16 @@ calc (k : R) = ↑(k % p + p * (k / p)) : by rw [nat.mod_add_div]
          ... = ↑(k % p)               : by simp [cast_eq_zero]
 
 /-- The characteristic of a finite ring cannot be zero. -/
-theorem char_ne_zero_of_fintype (p : ℕ) [hc : char_p R p] [fintype R] : p ≠ 0 :=
-assume h : p = 0,
-have char_zero R := @char_p_to_char_zero R _ (h ▸ hc),
-absurd (@nat.cast_injective R _ this) (not_injective_infinite_fintype coe)
+theorem char_ne_zero_of_finite (p : ℕ) [char_p R p] [finite R] : p ≠ 0 :=
+begin
+  unfreezingI { rintro rfl },
+  haveI : char_zero R := char_p_to_char_zero R,
+  casesI nonempty_fintype R,
+  exact absurd nat.cast_injective (not_injective_infinite_fintype (coe : ℕ → R))
+end
 
-lemma ring_char_ne_zero_of_fintype [fintype R] : ring_char R ≠ 0 :=
-char_ne_zero_of_fintype R (ring_char R)
+lemma ring_char_ne_zero_of_finite [finite R] : ring_char R ≠ 0 :=
+char_ne_zero_of_finite R (ring_char R)
 
 end
 
@@ -432,11 +435,11 @@ end semiring
 
 section ring
 
-variables (R) [ring R] [no_zero_divisors R] [nontrivial R] [fintype R]
+variables (R) [ring R] [no_zero_divisors R] [nontrivial R] [finite R]
 
 theorem char_is_prime (p : ℕ) [char_p R p] :
   p.prime :=
-or.resolve_right (char_is_prime_or_zero R p) (char_ne_zero_of_fintype R p)
+or.resolve_right (char_is_prime_or_zero R p) (char_ne_zero_of_finite R p)
 
 end ring
 

src/algebra/char_p/char_and_card.lean

@@ -15,12 +15,14 @@ We prove some results relating characteristic and cardinality of finite rings
 characterstic, cardinality, ring
 -/
 
-/-- A prime `p` is a unit in a finite commutative ring `R`
-iff it does not divide the characteristic. -/
-lemma is_unit_iff_not_dvd_char (R : Type*) [comm_ring R] [fintype R] (p : ℕ) [fact p.prime] :
+/-- A prime `p` is a unit in a commutative ring `R` of nonzero characterstic iff it does not divide
+the characteristic. -/
+lemma is_unit_iff_not_dvd_char_of_ring_char_ne_zero (R : Type*) [comm_ring R] (p : ℕ) [fact p.prime]
+  (hR : ring_char R ≠ 0) :
   is_unit (p : R) ↔ ¬ p ∣ ring_char R :=
 begin
   have hch := char_p.cast_eq_zero R (ring_char R),
+  have hp : p.prime := fact.out p.prime,
   split,
   { rintros h₁ ⟨q, hq⟩,
     rcases is_unit.exists_left_inv h₁ with ⟨a, ha⟩,
@@ -29,8 +31,7 @@ begin
       rintro ⟨r, hr⟩,
       rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq,
       nth_rewrite 0 ← mul_one (ring_char R) at hq,
-      exact nat.prime.not_dvd_one (fact.out p.prime)
-             ⟨r, mul_left_cancel₀ (char_p.char_ne_zero_of_fintype R (ring_char R)) hq⟩,
+      exact nat.prime.not_dvd_one hp ⟨r, mul_left_cancel₀ hR hq⟩,
     end,
     have h₄ := mt (char_p.int_cast_eq_zero_iff R (ring_char R) q).mp,
     apply_fun (coe : ℕ → R) at hq,
@@ -39,14 +40,19 @@ begin
     norm_cast at h₄,
     exact h₄ h₃ hq.symm, },
   { intro h,
-    rcases nat.is_coprime_iff_coprime.mpr ((nat.prime.coprime_iff_not_dvd (fact.out _)).mpr h)
-      with ⟨a, b, hab⟩,
+    rcases (hp.coprime_iff_not_dvd.mpr h).is_coprime with ⟨a, b, hab⟩,
     apply_fun (coe : ℤ → R) at hab,
     push_cast at hab,
     rw [hch, mul_zero, add_zero, mul_comm] at hab,
     exact is_unit_of_mul_eq_one (p : R) a hab, },
 end
 
+/-- A prime `p` is a unit in a finite commutative ring `R`
+iff it does not divide the characteristic. -/
+lemma is_unit_iff_not_dvd_char (R : Type*) [comm_ring R] (p : ℕ) [fact p.prime] [finite R] :
+  is_unit (p : R) ↔ ¬ p ∣ ring_char R :=
+is_unit_iff_not_dvd_char_of_ring_char_ne_zero R p $ char_p.char_ne_zero_of_finite R (ring_char R)
+
 /-- The prime divisors of the characteristic of a finite commutative ring are exactly
 the prime divisors of its cardinality. -/
 lemma prime_dvd_char_iff_dvd_card {R : Type*} [comm_ring R] [fintype R] (p : ℕ) [fact p.prime] :

src/ring_theory/coprime/lemmas.lean

@@ -33,6 +33,8 @@ theorem nat.is_coprime_iff_coprime {m n : ℕ} : is_coprime (m : ℤ) n ↔ nat.
 λ H, ⟨nat.gcd_a m n, nat.gcd_b m n, by rw [mul_comm _ (m : ℤ), mul_comm _ (n : ℤ),
     ← nat.gcd_eq_gcd_ab, show _ = _, from H, int.coe_nat_one]⟩⟩
 
+alias nat.is_coprime_iff_coprime ↔ is_coprime.nat_coprime nat.coprime.is_coprime
+
 theorem is_coprime.prod_left : (∀ i ∈ t, is_coprime (s i) x) → is_coprime (∏ i in t, s i) x :=
 finset.induction_on t (λ _, is_coprime_one_left) $ λ b t hbt ih H,
 by { rw finset.prod_insert hbt, rw finset.forall_mem_insert at H, exact H.1.mul_left (ih H.2) }