instIsReducedZModOfFactSquarefreeNat

Mathlib.RingTheory.ZMod

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

English

If n is squarefree (via a fact), then ZMod n is reduced.

Русский

Если n квадратно-разделимо, то ZMod n редуцирован.

LaTeX

$$$\\text{IsReduced}(\\\\mathbb{Z}/n\\\\mathbb{Z}) \\\\Rightarrow \\\\text{Squarefree}(n) \\\\lor n=0.$$$

Lean4

instance {n : ℕ} [Fact <| Squarefree n] : IsReduced (ZMod n) :=
  isReduced_zmod.2 <| Or.inl <| Fact.out

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

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

Разделы

Аффилиация

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