relfinrank_eq_one_of_le

Mathlib.FieldTheory.Relrank

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

English

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

Русский

Если B вложено в A (B ≤ A), то relfinrank(A,B) = 1.

LaTeX

$$$ B \le A \Rightarrow \operatorname{relfinrank}(A,B) = 1$$$

Lean4

theorem relfinrank_eq_one_of_le (h : B ≤ A) : relfinrank A B = 1 := by
  simp [relfinrank_eq_toNat_relrank, relrank_eq_one_of_le h]

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

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

Разделы

Аффилиация

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