expChar_prime

Mathlib.Algebra.CharP.Defs

URI: https://scilib.ai/kg/mathlib#expChar_prime

English

If p is a prime and CharP R p, then ExpChar R p holds.

Русский

Если p простое и CharP R p, то ExpChar R p выполняется.

LaTeX

$$CharP R p \Rightarrow ExpChar R p$$

Lean4

instance expChar_prime (p) [CharP R p] [Fact p.Prime] : ExpChar R p :=
  ExpChar.prime Fact.out

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

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

Разделы

Аффилиация

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