relrank_inf_mul_relrank — Mathlib

English

A general relation connecting inf-lattice and relrank: A.relrank(B ⊓ C) · B.relrank C = (A ⊓ B).relrank C.

Русский

Связь между inf и relrank: A.relrank(B ⊓ C) умножить на B.relrank C равно (A ⊓ B).relrank C.

LaTeX

$$$A, B, C \\text{ подполя} \\, E:\\\\ A.{\\rm relrank}(B \\sqcap C) \\cdot B.{\\rm relrank}(C) = (A \\sqcap B).{\\rm relrank}(C).$$$

Lean4

theorem relrank_inf_mul_relrank : A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C := by
  rw [← inf_relrank_right A (B ⊓ C), ← inf_relrank_right B C, ← inf_relrank_right (A ⊓ B) C, inf_assoc,
    relrank_mul_relrank inf_le_right inf_le_right]

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