expChar — Mathlib

English

For a domain ring R, ExpChar R (ringExpChar R) holds; i.e., ringExpChar gives a valid exponential characteristic.

Русский

Для кольца R с областю интегрируемых элементов, ExpChar R (ringExpChar R) выполняется; то есть ringExpChar задаёт допустимую экспоненциальную характеристику.

LaTeX

$$$\\\\ExpChar R (\\\\mathrm{ringExpChar}(R))$$$

Lean4

instance expChar [Ring R] [IsDomain R] : ExpChar R (ringExpChar R) :=
  by
  obtain ⟨q, _⟩ := ExpChar.exists R
  rwa [ringExpChar.eq R q]

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