compLocalizationAwayAlgHom_X_inl — Mathlib

English

The image of the X-inl generator under compLocalizationAwayAlgHom is mapped to the inverse of the corresponding quotient element in the localization away construction.

Русский

Образ генератора X_inl под compLocalizationAwayAlgHom равен обратному соответствующему элементу в конструировании локализации away.

LaTeX

$$$compLocalizationAwayAlgHom\\ _T g P (X (Sum.inl ())) = IsLocalization.Away.invSelf ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g))$$$

Lean4

@[simp]
theorem compLocalizationAwayAlgHom_X_inl :
    compLocalizationAwayAlgHom T g P (X (Sum.inl ())) =
      IsLocalization.Away.invSelf ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  by simp [compLocalizationAwayAlgHom]

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