finrank_mul_finrank — Mathlib

English

The finrank changes multiplicatively along towers: finrank_F K · finrank_K A = finrank_F A.

Русский

Финранк складывается по башне как произведение: finrank_F K · finrank_K A = finrank_F A.

LaTeX

$$$\\operatorname{finrank}_F K \\cdot \\operatorname{finrank}_K A = \\operatorname{finrank}_F A$$$

Lean4

/-- Tower law: if `A` is a `K`-module and `K` is an extension of `F` then
$\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$. -/
theorem finrank_mul_finrank : finrank F K * finrank K A = finrank F A :=
  by
  simp_rw [finrank]
  rw [← toNat_lift.{w} (Module.rank F K), ← toNat_lift.{v} (Module.rank K A), ← toNat_mul, lift_rank_mul_lift_rank,
    toNat_lift]

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