ofField_eq — Mathlib

English

The localization S of A at S, viewed as a subalgebra of K via Localization.subalgebra.ofField K S hS, satisfies the IsLocalization property; i.e., IsLocalization S (ofField K S hS) holds and coincides with the subalgebra structure coming from the field of fractions construction.

Русский

Локализация S A по S, рассматриваемая как подалгебра K через Localization.subalgebra.ofField K S hS, удовлетворяет свойству IsLocalization; то есть IsLocalization S (ofField K S hS) выполняется и совпадает с подалгебраической конструкцией из поля дробей.

LaTeX

$$$$ \text{IsLocalization } S \big(\operatorname{ofField} K S hS\big) $$$$

Lean4

theorem ofField_eq : ofField K S hS = subalgebra K S hS := by simp_rw [ofField, subalgebra, Subalgebra.copy_eq]

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