univ_eq_iUnion_image_add — Mathlib

English

A ring is a disjoint union of its cosets modulo an ideal.

Русский

Кольцо представляет собой дизъюнктное объединение своих косетов по идеалу.

LaTeX

$$$\mathrm{univ} = \bigcup_{x \in R/I} (x.out + I)$$$

Lean4

/-- A ring is made up of a disjoint union of cosets of an ideal. -/
theorem univ_eq_iUnion_image_add : (Set.univ (α := R)) = ⋃ x : R ⧸ I, x.out +ᵥ (I : Set R) :=
  QuotientAddGroup.univ_eq_iUnion_vadd I.toAddSubgroup

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