comp — Mathlib

English

If g and f have finite type, then their composition g ∘ f has finite type.

Русский

Если g и f имеют конечный тип, то их композиция g ∘ f тоже имеет конечный тип.

LaTeX

$$RingHom.FiniteType.comp hg hf : (g.comp f).FiniteType$$

Lean4

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

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