isLocalization_subalgebra — Mathlib

English

The instance asserts that the subalgebra constructed as Localization.subalgebra is itself a localization with respect to S.

Русский

Инстанс утверждает, что подалгебра, построенная как Localization.subalgebra, сама является локализацией по $S$.

LaTeX

$$$\\text{IsLocalization } S (Localization.subalgebra\\, K S hS)$$$

Lean4

instance isLocalization_subalgebra : IsLocalization S (subalgebra K S hS) :=
  by
  dsimp only [Localization.subalgebra]
  rw [Subalgebra.copy_eq]
  infer_instance

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