relrank_mul_rank_top — Mathlib

English

If A ≤ B, then relrank(A,B)·Module.rank(B,E) = Module.rank(A,E).

Русский

Если A ⊆ B, то relrank(A,B)·Module.rank(B,E) = Module.rank(A,E).

LaTeX

$$$ A \le B \Rightarrow \operatorname{relrank}(A,B) \cdot \operatorname{Module.rank}(B,E) = \operatorname{Module.rank}(A,E)$$$

Lean4

theorem relrank_mul_rank_top (h : A ≤ B) : relrank A B * Module.rank B E = Module.rank A E :=
  by
  rw [relrank_eq_rank_of_le h]
  letI : Algebra A B := (inclusion h).toAlgebra
  haveI : IsScalarTower A B E := IsScalarTower.of_algebraMap_eq' rfl
  exact rank_mul_rank A B E

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