inf_relfinrank_right

Mathlib.FieldTheory.Relrank

URI: https://scilib.ai/kg/mathlib#IntermediateField.inf_relfinrank_right

English

The right-infimum of relfinrank is stable: relfinrank((A ⊓ B), B) = relfinrank(A,B).

Русский

Правая инфиминальная часть сохраняется: relfinrank((A ⊓ B), B) = relfinrank(A,B).

LaTeX

$$$\\operatorname{relfinrank}(A \\sqcap B, B) = \\operatorname{relfinrank}(A,B).$$$

Lean4

theorem inf_relfinrank_right : relfinrank (A ⊓ B) B = relfinrank A B :=
  congr(toNat $(inf_relrank_right A B))

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

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

Разделы

Аффилиация

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