expChar_one_iff_char_zero — Mathlib

English

The exponential characteristic is one iff the characteristic is zero.

Русский

Экспоненциальная характеристика равна единице тогда и только тогда, когда характеристика равна нулю.

LaTeX

$$$\\\\forall R (p,q) [CharP R p] [ExpChar R q], q = 1 \\\\Leftrightarrow p = 0$$$

Lean4

/-- The exponential characteristic is one iff the characteristic is zero. -/
theorem expChar_one_iff_char_zero (p q : ℕ) [CharP R p] [ExpChar R q] : q = 1 ↔ p = 0 :=
  by
  constructor
  · rintro rfl
    exact char_zero_of_expChar_one R p
  · rintro rfl
    exact expChar_one_of_char_zero R q

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