comp_iff

Mathlib.RingTheory.EssentialFiniteness

URI: https://scilib.ai/kg/mathlib#Algebra.EssFiniteType.comp_iff

English

If R→S is EssFiniteType, then EssFiniteType R T is equivalent to EssFiniteType S T.

Русский

Если R→S имеет essFiniteType, то EssFiniteType R T эквивалентно EssFiniteType S T.

LaTeX

$$EssFiniteType R S ⇒ (EssFiniteType R T ↔ EssFiniteType S T)$$

Lean4

theorem comp_iff [EssFiniteType R S] : EssFiniteType R T ↔ EssFiniteType S T :=
  ⟨fun _ ↦ of_comp R S T, fun _ ↦ comp R S T⟩

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

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

Разделы

Аффилиация

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