quotientSpanEquivZMod — Mathlib

English

Let a be an integer. Then the quotient ring Z modulo the principal ideal generated by a is canonically isomorphic to Z/(|a|).

Русский

Пусть a — целое число. Тогда кольцо ℤ / ⟨a⟩ канонически изоморфно ℤ/(|a|).

LaTeX

$$$$\\mathbb{Z}/\\langle a \\rangle \\cong \\mathbb{Z}/|a|\\mathbb{Z}.$$$$

Lean4

/-- `ℤ` modulo the ideal generated by `a : ℤ` is `ZMod a.natAbs`. -/
def quotientSpanEquivZMod (a : ℤ) : ℤ ⧸ Ideal.span ({ a } : Set ℤ) ≃+* ZMod a.natAbs :=
  (Ideal.quotEquivOfEq (span_natAbs a)).symm.trans (quotientSpanNatEquivZMod a.natAbs)

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