relrank_comap — Mathlib

English

Relrank commutes with comap and map: relrank(A.comap f, B) = relrank(A, B.map f).

Русский

Relrank совместим с операциями comap и map: relrank(A.comap f, B) = relrank(A, B.map f).

LaTeX

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

Lean4

theorem relrank_comap {L : Type v} [Field L] (f : L →+* E) (B : Subfield L) :
    relrank (A.comap f) B = relrank A (B.map f) := by simpa only [lift_id] using A.lift_relrank_comap f B

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