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

$$$ B \le f.fieldRange \Rightarrow \operatorname{relfinrank}(A.comap f, B.comap f) = \operatorname{relfinrank}(A,B)$$$

Lean4

theorem relfinrank_comap_comap_eq_relfinrank_of_le (f : L →+* 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))

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