of_finite

Mathlib.RingTheory.FiniteType

URI: https://scilib.ai/kg/mathlib#RingHom.FiniteType.of_finite

English

If a ring homomorphism is finite, then it is of finite type.

Русский

Если гомоморфизм конечен, то он имеет конечный тип.

LaTeX

$$of_finite {f : RingHom A B} (hf : f.Finite) : f.FiniteType$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru