submonoid — Mathlib

English

The submonoid described above has the localization property that localizing S at it recovers S.

Русский

Указанное подмножество подмножества имеет свойство локализации: локализация S на нем восстанавливает S.

LaTeX

$$$IsLocalization\ (EssFiniteType.submonoid R S)\ S$$$

Lean4

/-- A submonoid of `EssFiniteType.subalgebra R S`, whose localization is the whole algebra `S`. -/
noncomputable def submonoid [EssFiniteType R S] : Submonoid (EssFiniteType.subalgebra R S) :=
  ((IsUnit.submonoid S).comap (algebraMap (EssFiniteType.subalgebra R S) S))

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