relrank_top_left

Mathlib.FieldTheory.Relrank

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

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.relrank (B \sqcap C) \cdot B.relrank C = A.relrank C $$$

Lean4

@[simp]
theorem relrank_top_left : relrank ⊤ A = 1 :=
  relrank_eq_one_of_le le_top

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

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

Разделы

Аффилиация

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