instIsSimpleAddGroup

Mathlib.GroupTheory.SpecificGroups.Cyclic

URI: https://scilib.ai/kg/mathlib#ZMod.instIsSimpleAddGroup

← MathLib Explorer

English

If p is prime, the additive group ZMod p is simple.

Русский

Пусть p простое, тогда аддитивная группа ZMod p простая.

LaTeX

$$IsSimpleAddGroup (ZMod p)$$

Lean4

instance instIsSimpleAddGroup {p : ℕ} [Fact p.Prime] : IsSimpleAddGroup (ZMod p) :=
  AddCommGroup.is_simple_iff_isAddCyclic_and_prime_card.2 ⟨inferInstance, by simpa using (Fact.out : p.Prime)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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