inseparableSetoid_ring — Mathlib

English

For a ring α with a topology making it a topological ring, the inseparable setoid equals the quotient relative to the closure of zero.

Русский

Для кольца α с топологией, делающее его топологическим кольцом, неразделимость (inseparable) совпадает с отношением эквивалентности по замыканию нуля.

LaTeX

$$$inseparableSetoid(\alpha) = Submodule.quotientRel (Ideal.closure ⊥)$$$

Lean4

theorem inseparableSetoid_ring (α) [Ring α] [TopologicalSpace α] [IsTopologicalRing α] :
    inseparableSetoid α = Submodule.quotientRel (Ideal.closure ⊥) :=
  Setoid.ext fun x y => addGroup_inseparable_iff.trans <| .trans (by rfl) (Submodule.quotientRel_def _).symm

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