relfinrank_mul_relfinrank — Mathlib

English

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

Русский

Если A ⊆ B ⊆ C, то relfinrank(A,B) умножить на relfinrank(B,C) равно relfinrank(A,C).

LaTeX

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

Lean4

theorem relfinrank_mul_relfinrank (h1 : A ≤ B) (h2 : B ≤ C) : relfinrank A B * relfinrank B C = relfinrank A C := by
  simpa using congr(toNat $(relrank_mul_relrank h1 h2))

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