relrank_inf_mul_relrank

Mathlib.FieldTheory.Relrank

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

← MathLib Explorer

English

For any A,B,C, relrank A (B ⊓ C) · relrank B C = (A ⊓ B).relrank C.

Русский

Для любых A,B,C выполняется: relrank A (B ⊓ C) · relrank B C = (A ⊓ B).relrank C.

LaTeX

$$$ A \relrank (B \sqcap C) \cdot B \relrank C = (A \sqcap B).relrank C $$$

Lean4

theorem relrank_inf_mul_relrank : A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C :=
  Subfield.relrank_inf_mul_relrank A.toSubfield B.toSubfield C.toSubfield

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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