rank_comap — Mathlib

English

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

Русский

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

LaTeX

$$$\operatorname{rank}(A \operatorname{comap} f) L = \operatorname{relrank}(A, f.fieldRange)$$$

Lean4

theorem rank_comap {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E) :
    Module.rank (A.comap f) L = relrank A f.fieldRange := by simpa only [lift_id] using A.lift_rank_comap f

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