relrank_inf_mul_relrank_of_le

Mathlib.FieldTheory.Relrank

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

← MathLib Explorer

English

For any A,B,C, relrank A (B ⊓ C) · B.relrank C = (A ⊓ B).relrank C.

Русский

Для любых A,B,C: relrank A (B ⊓ C) · B.relrank C = (A ⊓ B).relrank C.

LaTeX

$$$ A \relrank (B \sqcap C) \cdot B.relrank C = (A \sqcap B).relrank C $$$

Lean4

theorem relrank_inf_mul_relrank_of_le (h : A ≤ B) : A.relrank (B ⊓ C) * B.relrank C = A.relrank C := by
  simpa only [inf_of_le_left h] using relrank_inf_mul_relrank A B C

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

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

Разделы

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

Аффилиация

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