eq — Mathlib · SciLib

English

ringExpChar R equals q whenever ExpChar R q holds.

Русский

ringExpChar R равно q тогда, когда ExpChar R q выполняется.

LaTeX

$$$\\\\forall R [ ExpChar R q ] \\\\Rightarrow \\\\mathrm{ringExpChar}(R) = q$$$

Lean4

theorem eq (q : ℕ) [h : ExpChar R q] : ringExpChar R = q :=
  by
  rcases h with _ | h
  · haveI := CharP.ofCharZero R
    rw [ringExpChar, ringChar.eq R 0]; rfl
  rw [ringExpChar, ringChar.eq R q]
  exact Nat.max_eq_left h.one_lt.le

Похожие утверждения