relfinrank_comap_comap_eq_relfinrank_of_le

English

If B ≤ f.fieldRange, then relfinrank(A.comap f, B.comap f) = relfinrank A B.

Русский

Если B ≤ f.fieldRange, то relfinrank(A.comap f, B.comap f) = relfinrank A B.

LaTeX

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

Lean4

theorem relfinrank_comap_comap_eq_relfinrank_of_le (f : L →ₐ[F] E) (h : B ≤ f.fieldRange) :
    relfinrank (A.comap f) (B.comap f) = relfinrank A B := by
  simpa using congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_of_le A B f h))

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