comp_surjective — 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 comp_surjective {f : A →+* B} {g : B →+* C} (hf : f.FiniteType) (hg : Surjective g) : (g.comp f).FiniteType :=
  by
  algebraize_only  [f, g.comp f]
  exact
    ‹Algebra.FiniteType _ _›.of_surjective
      { g with
        toFun := g
        commutes' := fun a => rfl }
      hg

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