finiteType — Mathlib

English

If f: A → B and g: B → C are ring homomorphisms with f of finite type and g surjective, then the composition g ∘ f is of finite type.

Русский

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

LaTeX

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

Lean4

theorem finiteType {f : A →+* B} (hf : f.Finite) : FiniteType f :=
  @Module.Finite.finiteType _ _ _ _ f.toAlgebra hf

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