unitization_range — Mathlib

English

The range of the unitization map is the subalgebra generated by the closure of s as a ring.

Русский

Образ отображения единичизации есть подалгебра, порождаемая замыканием s как кольцо.

LaTeX

$$$\mathrm{range}(\mathrm{unitization}(s)) = \mathrm{subalgebraOfSubring}(\mathrm{Subring.closure}(s))$$$

Lean4

theorem unitization_range : (unitization s).range = subalgebraOfSubring (.closure s) :=
  by
  have := AddSubgroupClass.zsmulMemClass (S := S)
  rw [unitization, NonUnitalSubalgebra.unitization_range (hSRA := this), Algebra.adjoin_int]

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