relrank_dvd_of_le_left

Mathlib.FieldTheory.Relrank

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

English

For any A ≤ B, B.relrank C divides A.relrank C.

Русский

Для любых A ≤ B выполняется, что B.relrank C делит A.relrank C.

LaTeX

$$$ A \le B \Rightarrow B.relrank C \ \mid \ A.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