relrank_inf_mul_relrank_of_le

Mathlib.FieldTheory.Relrank

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

← MathLib Explorer

English

If A ≤ B, then A.relrank(B ⊓ C) · B.relrank C = A.relrank C.

Русский

Если A ≤ B, то A.relrank(B ⊓ C) · B.relrank C = A.relrank C.

LaTeX

$$$A \\le B \\Rightarrow A.{\\rm relrank}(B \\sqcap C) \\cdot B.{\\rm relrank}(C) = A.{\\rm relrank}(C).$$$

Lean4

theorem relrank_inf_mul_relrank_of_le (h : A ≤ B) : A.relrank (B ⊓ C) * B.relrank C = A.relrank C := by
  simpa only [inf_of_le_left h] using relrank_inf_mul_relrank A B C

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

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

Разделы

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

Аффилиация

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