relfinrank_dvd_finrank_bot

Mathlib.FieldTheory.Relrank

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

← MathLib Explorer

English

For any A ⊆ B, relfinrank A B divides finrank F B.

Русский

Для любых A ⊆ B, relfinrank A B делит finrank F B.

LaTeX

$$$ \operatorname{relfinrank} A B \ \mid \ \operatorname{finrank} F B $$$

Lean4

theorem relfinrank_dvd_finrank_bot : relfinrank A B ∣ finrank F B :=
  inf_relfinrank_right A B ▸ dvd_of_mul_left_eq _ (finrank_bot_mul_relfinrank inf_le_right)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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