inf_relfinrank_right

Mathlib.FieldTheory.Relrank

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

English

relfinrank(A ∩ B) B = relfinrank A B.

Русский

relfinrank(A ∩ B) B = relfinrank A B.

LaTeX

$$$\\mathrm{relfinrank}(A \\cap B) B = \\mathrm{relfinrank} A B$$$

Lean4

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

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

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

Разделы

Аффилиация

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