English
Let R be a ring and I a two-sided ideal. The quotient relation modulo I is a ring congruence, so the quotient R/I inherits a natural ring structure and the quotient map is a surjective ring homomorphism.
Русский
Пусть R — кольцо и I — двусторонний идеал. Отношение тождественности по модулю I является кольцевой конгруэнцией, поэтому фактор-кольцо R/I естественным образом наделяется кольцом, и естественный фактор-мономорфизм является сюръективным кольмовомоморфизмом.
LaTeX
$$$\\forall a,b,c,d \\in R,\\ a \\equiv b \\pmod{I}\\ \\land\\ c \\equiv d \\pmod{I} \\Rightarrow a+c \\equiv b+d \\pmod{I} \\land\\ ac \\equiv bd \\pmod{I}$$$
Lean4
/-- On `Ideal`s, `Submodule.quotientRel` is a ring congruence. -/
protected def ringCon (I : Ideal R) [I.IsTwoSided] : RingCon R
where
__ := QuotientAddGroup.con I.toAddSubgroup
mul' {a₁ b₁ a₂ b₂} h₁
h₂ := by
rw [Submodule.quotientRel_def] at h₁ h₂ ⊢
exact mul_sub_mul_mem I h₁ h₂
