feat(Algebra/CharP/*): add RingHom.(charP|expChar)[_iff] (#10574)

similar to `RingHom.charZero[_iff]`

Mathlib/Algebra/CharP/Algebra.lean

@@ -31,8 +31,8 @@ Instances constructed from this result:
 
 
 /-- If a ring homomorphism `R →+* A` is injective then `A` has the same characteristic as `R`. -/
-theorem charP_of_injective_ringHom {R A : Type*} [Semiring R] [Semiring A] {f : R →+* A}
-    (h : Function.Injective f) (p : ℕ) [CharP R p] : CharP A p where
+theorem charP_of_injective_ringHom {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A]
+    {f : R →+* A} (h : Function.Injective f) (p : ℕ) [CharP R p] : CharP A p where
   cast_eq_zero_iff' x := by
     rw [← CharP.cast_eq_zero_iff R p x, ← map_natCast f x, map_eq_zero_iff f h]
 
@@ -49,8 +49,8 @@ theorem charP_of_injective_algebraMap' (R A : Type*) [Field R] [Semiring A] [Alg
 
 /-- If a ring homomorphism `R →+* A` is injective and `R` has characteristic zero
 then so does `A`. -/
-theorem charZero_of_injective_ringHom {R A : Type*} [Semiring R] [Semiring A] {f : R →+* A}
-    (h : Function.Injective f) [CharZero R] : CharZero A where
+theorem charZero_of_injective_ringHom {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A]
+    {f : R →+* A} (h : Function.Injective f) [CharZero R] : CharZero A where
   cast_injective _ _ _ := CharZero.cast_injective <| h <| by simpa only [map_natCast f]
 
 /-- If the algebra map `R →+* A` is injective and `R` has characteristic zero then so does `A`. -/
@@ -59,6 +59,19 @@ theorem charZero_of_injective_algebraMap {R A : Type*} [CommSemiring R] [Semirin
   charZero_of_injective_ringHom h
 #align char_zero_of_injective_algebra_map charZero_of_injective_algebraMap
 
+/-- If `R →+* A` is injective, and `A` is of characteristic `p`, then `R` is also of
+characteristic `p`. Similar to `RingHom.charZero`. -/
+theorem RingHom.charP {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A)
+    (H : Function.Injective f) (p : ℕ) [CharP A p] : CharP R p := by
+  obtain ⟨q, h⟩ := CharP.exists R
+  exact CharP.eq _ (charP_of_injective_ringHom H q) ‹CharP A p› ▸ h
+
+/-- If `R →+* A` is injective, then `R` is of characteristic `p` if and only if `A` is also of
+characteristic `p`. Similar to `RingHom.charZero_iff`. -/
+theorem RingHom.charP_iff {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A)
+    (H : Function.Injective f) (p : ℕ) : CharP R p ↔ CharP A p :=
+  ⟨fun _ ↦ charP_of_injective_ringHom H p, fun _ ↦ f.charP H p⟩
+
 /-!
 As an application, a `ℚ`-algebra has characteristic zero.
 -/

Mathlib/Algebra/CharP/ExpChar.lean

@@ -188,6 +188,20 @@ theorem expChar_of_injective_ringHom {R A : Type*}
   · haveI := charZero_of_injective_ringHom h; exact .zero
   haveI := charP_of_injective_ringHom h q; exact .prime hprime
 
+/-- If `R →+* A` is injective, and `A` is of exponential characteristic `p`, then `R` is also of
+exponential characteristic `p`. Similar to `RingHom.charZero`. -/
+theorem RingHom.expChar {R A : Type*} [Semiring R] [Semiring A] (f : R →+* A)
+    (H : Function.Injective f) (p : ℕ) [ExpChar A p] : ExpChar R p := by
+  cases ‹ExpChar A p› with
+  | zero => haveI := f.charZero; exact .zero
+  | prime hp => haveI := f.charP H p; exact .prime hp
+
+/-- If `R →+* A` is injective, then `R` is of exponential characteristic `p` if and only if `A` is
+also of exponential characteristic `p`. Similar to `RingHom.charZero_iff`. -/
+theorem RingHom.expChar_iff {R A : Type*} [Semiring R] [Semiring A] (f : R →+* A)
+    (H : Function.Injective f) (p : ℕ) : ExpChar R p ↔ ExpChar A p :=
+  ⟨fun _ ↦ expChar_of_injective_ringHom H p, fun _ ↦ f.expChar H p⟩
+
 /-- If the algebra map `R →+* A` is injective then `A` has the same exponential characteristic
 as `R`. -/
 theorem expChar_of_injective_algebraMap {R A : Type*}