feat(Algebra/CharP/ExpChar): add expChar[_pow]_pos (#9260)

... which states that (the power of) exponential characteristic is positive.
leanprover-community · Dec 25, 2023 · 5ca2c4b · 5ca2c4b
1 parent c26c85d
commit 5ca2c4b
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/Mathlib/Algebra/CharP/ExpChar.lean b/Mathlib/Algebra/CharP/ExpChar.lean
@@ -107,6 +107,15 @@ theorem expChar_is_prime_or_one (q : ℕ) [hq : ExpChar R q] : Nat.Prime q ∨ q
   case prime hp _ => exact .inl hp
 #align exp_char_is_prime_or_one expChar_is_prime_or_one
 
+/-- The exponential characteristic is positive. -/
+theorem expChar_pos (q : ℕ) [ExpChar R q] : 0 < q := by
+  rcases expChar_is_prime_or_one R q with h | rfl
+  exacts [Nat.Prime.pos h, Nat.one_pos]
+
+/-- Any power of the exponential characteristic is positive. -/
+theorem expChar_pow_pos (q : ℕ) [ExpChar R q] (n : ℕ) : 0 < q ^ n :=
+  Nat.pos_pow_of_pos n (expChar_pos R q)
+
 end NoZeroDivisors
 
 end Nontrivial