Quotient_Ring_of_Integers_and_Principal_Ideal_from_Unity
Provedintegersproofwikiquotient-ringring-theory
Let be the integral domain of integers. Let be the principal ideal of generated by . The quotient ring is isomorphic to the null ring.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.RingTheory.Ideal.Quotient.Basic
Formal statement
theorem Quotient_Ring_of_Integers_and_Principal_Ideal_from_Unity : ∀ x : ℤ ⧸ (Ideal.span ({1} : Set ℤ)), x = 0 := by sorrySource