relrank_dvd_of_le_left

Mathlib.FieldTheory.Relrank

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

English

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

Русский

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

LaTeX

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

Lean4

theorem relrank_dvd_of_le_left (h : A ≤ B) : B.relrank C ∣ A.relrank C :=
  dvd_of_mul_left_eq _ (relrank_inf_mul_relrank_of_le C h)

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

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

Разделы

Аффилиация

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