comp — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall g:\\, B \\to C\\; f:\\, A \\to B,\\; g.Finite \\land f.Finite \\Rightarrow (g \\circ f).Finite$$$

Lean4

theorem comp {g : B →+* C} {f : A →+* B} (hg : g.Finite) (hf : f.Finite) : (g.comp f).Finite :=
  by
  algebraize [f, g, g.comp f]
  exact Module.Finite.trans B C

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