finite_stableUnderComposition

Mathlib.RingTheory.RingHom.Finite

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

English

Finite is stable under composition.

Русский

конечность стабильна под композициями.

LaTeX

$$$\\operatorname{StableUnderComposition}(\\text{Finite})$$$

Lean4

theorem finite_stableUnderComposition : StableUnderComposition @Finite :=
  by
  introv R hf hg
  exact hg.comp hf

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

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

Разделы

Аффилиация

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