English
If A ≤ B ≤ C, then relrank(A,B) · relrank(B,C) = relrank(A,C).
Русский
Если A ⊆ B ⊆ C, то relrank(A,B) умноженное на relrank(B,C) даёт relrank(A,C).
LaTeX
$$$A \\le B \\le C \\implies \\operatorname{relrank}(A,B) \\cdot \\operatorname{relrank}(B,C) = \\operatorname{relrank}(A,C).$$$
Lean4
theorem relrank_mul_relrank (h1 : A ≤ B) (h2 : B ≤ C) : relrank A B * relrank B C = relrank A C :=
by
have h3 := h1.trans h2
rw [relrank_eq_rank_of_le h1, relrank_eq_rank_of_le h2, relrank_eq_rank_of_le h3]
letI : Algebra A B := (inclusion h1).toAlgebra
letI : Algebra B C := (inclusion h2).toAlgebra
letI : Algebra A C := (inclusion h3).toAlgebra
haveI : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' rfl
exact rank_mul_rank A B C
