finiteType_holdsForLocalizationAway

English

HoldsForLocalizationAway: the localization away preserves FP when looking at finite type.

Русский

HoldsForLocalizationAway: локализация Away сохраняет FP для локализаций конечного типа.

LaTeX

$$$\text{HoldsForLocalizationAway }\operatorname{FiniteType}$$$

Lean4

theorem finiteType_holdsForLocalizationAway : HoldsForLocalizationAway @FiniteType :=
  by
  introv R _
  rw [finiteType_algebraMap]
  exact IsLocalization.finiteType_of_monoid_fg (Submonoid.powers r) S

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