of_comp_finiteType — Mathlib

English

If the composition (g ∘ f) has finite type, then g has finite type.

Русский

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

LaTeX

$$of_comp_finiteType {f} {g} (h : (g.comp f).FiniteType) : g.FiniteType$$

Lean4

theorem of_comp_finiteType {f : A →+* B} {g : B →+* C} (h : (g.comp f).FiniteType) : g.FiniteType :=
  by
  algebraize [f, g, g.comp f]
  exact Algebra.FiniteType.of_restrictScalars_finiteType A B C

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