relfinrank_comap — Mathlib

English

Relfinrank commutes with comap and map: relfinrank(A.comap f, B) = relfinrank(A, B.map f).

Русский

Relfinrank совместим с comap и map: relfinrank(A.comap f, B) = relfinrank(A, B.map f).

LaTeX

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

Lean4

theorem relfinrank_comap (f : L →+* E) (B : Subfield L) : relfinrank (A.comap f) B = relfinrank A (B.map f) := by
  simpa using congr(toNat $(lift_relrank_comap A f B))

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