two_le_char

Mathlib.Data.ZMod.Basic

URI: https://scilib.ai/kg/mathlib#ZModModule.two_le_char

English

If n is nonzero and G is nontrivial, then 2 ≤ n; equivalently the characteristic of the ZMod n-module cannot be 1.

Русский

Если n не равно нулю и G не тривиальна, то 2 ≤ n; иначе характеристика модуля ZMod n не может быть равной 1.

LaTeX

$$$2 \le n$$$

Lean4

theorem two_le_char [NeZero n] [Nontrivial G] : 2 ≤ n :=
  by
  have := NeZero.ne n
  have := char_ne_one n G
  cutsat

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

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

Разделы

Аффилиация

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