of_eq

Mathlib.Algebra.CharP.Defs

URI: https://scilib.ai/kg/mathlib#ringExpChar.of_eq

English

If ringExpChar R = q, then ExpChar R q.

Русский

Если ringExpChar R = q, тогда ExpChar R q.

LaTeX

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

Lean4

theorem of_eq [Ring R] [IsDomain R] {q : ℕ} (h : ringExpChar R = q) : ExpChar R q :=
  h ▸ ringExpChar.expChar R

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru