relrank_eq_one_of_le

Mathlib.FieldTheory.Relrank

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

English

If B is contained in A, then relrank(A,B) = 1.

Русский

Если B содержится в A, то relrank(A,B) = 1.

LaTeX

$$$B \le A \;\Rightarrow\; \operatorname{relrank} A B = 1$$$

Lean4

theorem relrank_eq_one_of_le (h : B ≤ A) : relrank A B = 1 := by
  rw [← inf_relrank_right, inf_eq_right.2 h, relrank_self]

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

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

Разделы

Аффилиация

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