relrank_eq_one_of_le

Mathlib.FieldTheory.Relrank

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

English

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

Русский

Если B вложено в A (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