feat: port Algebra.CharP.CharAndCard (#3285)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Mathlib.lean

@@ -35,6 +35,7 @@ import Mathlib.Algebra.Category.GroupCat.Zero
 import Mathlib.Algebra.Category.MonCat.Basic
 import Mathlib.Algebra.CharP.Algebra
 import Mathlib.Algebra.CharP.Basic
+import Mathlib.Algebra.CharP.CharAndCard
 import Mathlib.Algebra.CharP.ExpChar
 import Mathlib.Algebra.CharP.Invertible
 import Mathlib.Algebra.CharP.Pi

Mathlib/Algebra/CharP/CharAndCard.lean

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2022 Michael Stoll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Stoll
+
+! This file was ported from Lean 3 source module algebra.char_p.char_and_card
+! leanprover-community/mathlib commit 2fae5fd7f90711febdadf19c44dc60fae8834d1b
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.CharP.Basic
+import Mathlib.GroupTheory.Perm.Cycle.Type
+
+/-!
+# Characteristic and cardinality
+
+We prove some results relating characteristic and cardinality of finite rings
+
+## Tags
+characterstic, cardinality, ring
+-/
+
+
+/-- A prime `p` is a unit in a commutative ring `R` of nonzero characterstic iff it does not divide
+the characteristic. -/
+theorem isUnit_iff_not_dvd_char_of_ringChar_ne_zero (R : Type _) [CommRing R] (p : ℕ) [Fact p.Prime]
+    (hR : ringChar R ≠ 0) : IsUnit (p : R) ↔ ¬p ∣ ringChar R := by
+  have hch := CharP.cast_eq_zero R (ringChar R)
+  have hp : p.Prime := Fact.out
+  constructor
+  · rintro h₁ ⟨q, hq⟩
+    rcases IsUnit.exists_left_inv h₁ with ⟨a, ha⟩
+    have h₃ : ¬ringChar R ∣ q := by
+      rintro ⟨r, hr⟩
+      rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq
+      nth_rw 1 [← mul_one (ringChar R)] at hq
+      exact Nat.Prime.not_dvd_one hp ⟨r, mul_left_cancel₀ hR hq⟩
+    have h₄ := mt (CharP.int_cast_eq_zero_iff R (ringChar R) q).mp
+    apply_fun ((↑) : ℕ → R)  at hq
+    apply_fun (· * ·) a  at hq
+    rw [Nat.cast_mul, hch, MulZeroClass.mul_zero, ← mul_assoc, ha, one_mul] at hq
+    norm_cast  at h₄
+    exact h₄ h₃ hq.symm
+  · intro h
+    rcases(hp.coprime_iff_not_dvd.mpr h).isCoprime with ⟨a, b, hab⟩
+    apply_fun ((↑) : ℤ → R)  at hab
+    push_cast at hab
+    rw [hch, MulZeroClass.mul_zero, add_zero, mul_comm] at hab
+    exact isUnit_of_mul_eq_one (p : R) a hab
+#align is_unit_iff_not_dvd_char_of_ring_char_ne_zero isUnit_iff_not_dvd_char_of_ringChar_ne_zero
+
+/-- A prime `p` is a unit in a finite commutative ring `R`
+iff it does not divide the characteristic. -/
+theorem isUnit_iff_not_dvd_char (R : Type _) [CommRing R] (p : ℕ) [Fact p.Prime] [Finite R] :
+    IsUnit (p : R) ↔ ¬p ∣ ringChar R :=
+  isUnit_iff_not_dvd_char_of_ringChar_ne_zero R p <| CharP.char_ne_zero_of_finite R (ringChar R)
+#align is_unit_iff_not_dvd_char isUnit_iff_not_dvd_char
+
+/-- The prime divisors of the characteristic of a finite commutative ring are exactly
+the prime divisors of its cardinality. -/
+theorem prime_dvd_char_iff_dvd_card {R : Type _} [CommRing R] [Fintype R] (p : ℕ) [Fact p.Prime] :
+    p ∣ ringChar R ↔ p ∣ Fintype.card R := by
+  refine'
+    ⟨fun h =>
+      h.trans <|
+        Int.coe_nat_dvd.mp <|
+          (CharP.int_cast_eq_zero_iff R (ringChar R) (Fintype.card R)).mp <| by
+            exact_mod_cast CharP.cast_card_eq_zero R,
+      fun h => _⟩
+  by_contra h₀
+  rcases exists_prime_addOrderOf_dvd_card p h with ⟨r, hr⟩
+  have hr₁ := addOrderOf_nsmul_eq_zero r
+  rw [hr, nsmul_eq_mul] at hr₁
+  rcases IsUnit.exists_left_inv ((isUnit_iff_not_dvd_char R p).mpr h₀) with ⟨u, hu⟩
+  apply_fun (· * ·) u  at hr₁
+  rw [MulZeroClass.mul_zero, ← mul_assoc, hu, one_mul] at hr₁
+  exact mt AddMonoid.addOrderOf_eq_one_iff.mpr (ne_of_eq_of_ne hr (Nat.Prime.ne_one Fact.out)) hr₁
+#align prime_dvd_char_iff_dvd_card prime_dvd_char_iff_dvd_card
+
+/-- A prime that does not divide the cardinality of a finite commutative ring `R`
+is a unit in `R`. -/
+theorem not_isUnit_prime_of_dvd_card {R : Type _} [CommRing R] [Fintype R] (p : ℕ) [Fact p.Prime]
+    (hp : p ∣ Fintype.card R) : ¬IsUnit (p : R) :=
+  mt (isUnit_iff_not_dvd_char R p).mp
+    (Classical.not_not.mpr ((prime_dvd_char_iff_dvd_card p).mpr hp))
+#align not_is_unit_prime_of_dvd_card not_isUnit_prime_of_dvd_card