relfinrank_inf_mul_relfinrank

Mathlib.FieldTheory.Relrank

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem relfinrank_inf_mul_relfinrank : A.relfinrank (B ⊓ C) * B.relfinrank C = (A ⊓ B).relfinrank C := by
  simpa using congr(toNat $(relrank_inf_mul_relrank A B C))

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

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

Разделы

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

Аффилиация

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