finiteType_respectsIso — Mathlib

English

Finite type is preserved by ring isomorphisms.

Русский

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

LaTeX

$$$\operatorname{finiteType\_respectsIso}$$$

Lean4

theorem finiteType_respectsIso : RingHom.RespectsIso @RingHom.FiniteType :=
  by
  refine finiteType_stableUnderComposition.respectsIso (fun {R S} _ _ e ↦ ?_)
  algebraize [e.toRingHom]
  apply Algebra.FiniteType.equiv (inferInstanceAs <| Algebra.FiniteType R R) <| .ofRingEquiv (congrFun rfl)

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