relfinrank_inf_mul_relfinrank_of_le

English

If A ≤ B, then relfinrank A (B ⊓ C) · relfinrank B C = relfinrank A C.

Русский

Если A ≤ B, то relfinrank A (B ⊓ C) · relfinrank B C = relfinrank A C.

LaTeX

$$$A \\le B \\Rightarrow \\operatorname{relfinrank}(A, B \\sqcap C) \\cdot \\operatorname{relfinrank}(B, C) = \\operatorname{relfinrank}(A, C).$$$

Lean4

theorem relfinrank_inf_mul_relfinrank_of_le (h : A ≤ B) : A.relfinrank (B ⊓ C) * B.relfinrank C = A.relfinrank C := by
  simpa using congr(toNat $(relrank_inf_mul_relrank_of_le C h))

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