finiteType_isStableUnderBaseChange

English

Finite type is stable under base change (another base ring).

Русский

Конечный тип сохраняется при базовом изменении (при смене основания).

LaTeX

$$$\text{IsStableUnderBaseChange }\operatorname{FiniteType}$$$

Lean4

theorem finiteType_isStableUnderBaseChange : IsStableUnderBaseChange @FiniteType :=
  by
  apply IsStableUnderBaseChange.mk
  · exact finiteType_respectsIso
  · introv h
    rw [finiteType_algebraMap] at h
    suffices Algebra.FiniteType S (S ⊗[R] T) by rw [RingHom.FiniteType]; convert this; ext; simp_rw [Algebra.smul_def];
      rfl
    infer_instance

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