relfinrank_inf_mul_relfinrank — Mathlib

English

The natural version of the previous relation: relfinrank(A, B ⊓ C) · relfinrank(B, C) = (A ⊓ B).relfinrank C.

Русский

Натуральная версия предшествующего соотношения: relfinrank(A, B ⊓ C) · relfinrank(B, C) = (A ⊓ B).relfinrank C.

LaTeX

$$$A, B, C \\text{ подполя} \\, E:\\\\ \\operatorname{relfinrank}(A, B \\sqcap C) \\cdot \\operatorname{relfinrank}(B, C) = \\operatorname{relfinrank}(A \\sqcap B, 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))

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