comp — Mathlib

English

If g and f are finite, then their composition g ∘ f is finite.

Русский

Если g и f конечны как алгебра-гомоморфии, то их композиция действительно конечна.

LaTeX

$$$\\\\forall R A B C \\, [\\\\text{CommRing } R] \, [\\\\text{CommRing } A] \, [\\\\text{CommRing } B] \, [\\\\text{CommRing } C], \\\\ f:A \\to_[R] B, \\\\ g:B \\to_[R] C, \\\\ g.Finite \\Rightarrow f.Finite \\Rightarrow (g \\circ f).Finite.$$$

Lean4

theorem comp {g : B →ₐ[R] C} {f : A →ₐ[R] B} (hg : g.Finite) (hf : f.Finite) : (g.comp f).Finite :=
  RingHom.Finite.comp hg hf

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