finrank_comap — Mathlib

English

For a field homomorphism f, the finrank of (A.comap f) over L equals relfinrank A against f.fieldRange.

Русский

Для гомоморфизма f конечная размерность (A.comap f) над L равна relfinrank(A, f.fieldRange).

LaTeX

$$$\operatorname{finrank}(A \operatorname{comap} f) L = \operatorname{relfinrank}(A, f.fieldRange)$$$

Lean4

theorem finrank_comap (f : L →ₐ[F] E) : finrank (A.comap f) L = relfinrank A f.fieldRange := by
  simpa using congr(toNat $(lift_rank_comap A f))

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