From 039d0c764222c952a7433440024a4adb1aaebaba Mon Sep 17 00:00:00 2001
From: Suzuka Yu <109365723+Yu-Misaka@users.noreply.github.com>
Date: Sun, 12 Jan 2025 21:56:32 +0000
Subject: [PATCH] doc(Mathlib/Algebra/CharP/LinearMaps.lean): Fix doc errors
 (#20679)

1. Fix the doc-string of `Mathlib/Algebra/CharP/LinearMaps.lean`: the name `CharP_if` is outdated and is now corrected as `Module.charP_end`.
2. Express the condition of `Module.charP_end` in the term of torsion.
---
 Mathlib/Algebra/CharP/LinearMaps.lean | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Algebra/CharP/LinearMaps.lean b/Mathlib/Algebra/CharP/LinearMaps.lean
index 36f3baf18a80d..93009eaa7324f 100644
--- a/Mathlib/Algebra/CharP/LinearMaps.lean
+++ b/Mathlib/Algebra/CharP/LinearMaps.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wanyi He, Huanyu Zheng
 -/
 import Mathlib.Algebra.CharP.Algebra
+import Mathlib.Algebra.Module.Torsion
 /-!
 # Characteristic of the ring of linear Maps
 
@@ -12,10 +13,9 @@ The characteristic of the ring of linear maps is determined by its base ring.
 
 ## Main Results
 
-- `CharP_if` : For a commutative semiring `R` and a `R`-module `M`,
+- `Module.charP_end` : For a commutative semiring `R` and a `R`-module `M`,
   the characteristic of `R` is equal to the characteristic of the `R`-linear
-  endomorphisms of `M` when `M` contains an element `x` such that
-  `r • x = 0` implies `r = 0`.
+  endomorphisms of `M` when `M` contains a non-torsion element `x`.
 
 ## Notations
 
@@ -26,7 +26,7 @@ The characteristic of the ring of linear maps is determined by its base ring.
 
 One can also deduce similar result via `charP_of_injective_ringHom` and
   `R → (M →ₗ[R] M) : r ↦ (fun (x : M) ↦ r • x)`. But this will require stronger condition
-  compared to `CharP_if`.
+  compared to `Module.charP_end`.
 
 -/
 
@@ -35,12 +35,14 @@ namespace Module
 variable {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M]
 
 /-- For a commutative semiring `R` and a `R`-module `M`, if `M` contains an
-  element `x` such that `r • x = 0` implies `r = 0` (finding such element usually
-  depends on specific `•`), then the characteristic of `R` is equal to the
+  element `x` that is not torsion, then the characteristic of `R` is equal to the
   characteristic of the `R`-linear endomorphisms of `M`.-/
 theorem charP_end {p : ℕ} [hchar : CharP R p]
-    (hreduction : ∃ x : M, ∀ r : R, r • x = 0 → r = 0) : CharP (M →ₗ[R] M) p where
+    (htorsion : ∃ x : M, Ideal.torsionOf R M x = ⊥) : CharP (M →ₗ[R] M) p where
   cast_eq_zero_iff' n := by
+    have hreduction : ∃ x : M, ∀ r : R, r • x = 0 → r = 0 :=
+      Exists.casesOn htorsion fun x hx ↦
+        Exists.intro x fun r a ↦ (hx ▸ Ideal.mem_torsionOf_iff x r).mpr a
     have exact : (n : M →ₗ[R] M) = (n : R) • 1 := by
       simp only [Nat.cast_smul_eq_nsmul, nsmul_eq_mul, mul_one]
     rw [exact, LinearMap.ext_iff, ← hchar.1]