relfinrank_dvd_of_le_left

Mathlib.FieldTheory.Relrank

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

English

If A ≤ B, then B.relfinrank C divides A.relfinrank C.

Русский

Если A ≤ B, то B.relfinrank C делит A.relfinrank C.

LaTeX

$$$A \\le B \\Rightarrow B.{\\rm relfinrank}(C) \\;|\\; A.{\\rm relfinrank}(C).$$$

Lean4

theorem relfinrank_dvd_of_le_left (h : A ≤ B) : B.relfinrank C ∣ A.relfinrank C :=
  dvd_of_mul_left_eq _ (relfinrank_inf_mul_relfinrank_of_le C h)

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

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

Разделы

Аффилиация

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