finiteType_stableUnderComposition

Mathlib.RingTheory.RingHom.FiniteType

URI: https://scilib.ai/kg/mathlib#RingHom.finiteType_stableUnderComposition

English

Finite type/stability under composition: if two maps are FP, their composition is FP.

Русский

Конечный тип/стабильность при композиции: если два отображения FP, их композиция FP.

LaTeX

$$$\text{StableUnderComposition }\operatorname{FiniteType}$$$

Lean4

theorem finiteType_stableUnderComposition : StableUnderComposition @FiniteType :=
  by
  introv R hf hg
  exact hg.comp hf

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

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

Разделы

Аффилиация

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