comp — Mathlib

English

If g and f are algebra homomorphisms of finite type, then their composition g ∘ f is of finite type.

Русский

Если g и f — алгебраические гомоморфизмы конечного типа, то их композиция конечна по порождению.

LaTeX

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

Lean4

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

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