val_eq_one

Mathlib.Data.ZMod.Basic

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

← MathLib Explorer

English

Nontriviality of ZMod n is equivalent to n ≠ 1.

Русский

Неприводимость ZMod n эквивалентна n ≠ 1.

LaTeX

$$$\text{Nontrivial}(\mathbb{Z}/n\mathbb{Z}) \iff n \neq 1$$$

Lean4

theorem val_eq_one : ∀ {n : ℕ} (_ : 1 < n) (a : ZMod n), a.val = 1 ↔ a = 1
  | 0, hn, _ | 1, hn, _ => by simp at hn
  | n + 2, _, _ => by simp only [val, ZMod, Fin.ext_iff, Fin.val_one]

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

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

Разделы

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

Аффилиация

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