finite_isStableUnderBaseChange — Mathlib

English

Finite is stable under base change for ring homomorphisms.

Русский

Конечность устойчива к базовым изменениям для кольцевых гомоморфизмов.

LaTeX

$$$\\operatorname{IsStableUnderBaseChange}(\\text{Finite})$$$

Lean4

theorem finite_isStableUnderBaseChange : IsStableUnderBaseChange @Finite :=
  by
  refine IsStableUnderBaseChange.mk finite_respectsIso ?_
  classical
  introv h
  replace h : Module.Finite R T := by rw [RingHom.Finite] at h; convert h; ext; simp_rw [Algebra.smul_def]; rfl
  suffices Module.Finite S (S ⊗[R] T) by rw [RingHom.Finite]; convert this; congr; ext; simp_rw [Algebra.smul_def]; rfl
  exact inferInstance

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