relfinrank_comap — Mathlib

English

The relative finite rank of (A.comap f) with B equals the relative finite rank of A with B.map f.

Русский

Относительная конечная размерность (A.comap f) с B равна relfinrank(A, B.map f).

LaTeX

$$$\operatorname{relfinrank}(A \operatorname{comap} f, B) = \operatorname{relfinrank}(A, B.map f)$$$

Lean4

theorem relfinrank_comap (f : L →ₐ[F] E) (B : IntermediateField F L) :
    relfinrank (A.comap f) B = relfinrank A (B.map f) := by simpa using congr(toNat $(lift_relrank_comap A f B))

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