relrank_comap_comap_eq_relrank_inf

English

The relrank of (A.comap f) with (B.comap f) equals relrank of A with B ∩ f.fieldRange.

Русский

Relrank (A.comap f) (B.comap f) = Relrank(A, B ∩ f.fieldRange).

LaTeX

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

Lean4

theorem relrank_comap_comap_eq_relrank_inf {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E) :
    relrank (A.comap f) (B.comap f) = relrank A (B ⊓ f.fieldRange) := by
  simpa only [lift_id] using lift_relrank_comap_comap_eq_lift_relrank_inf A B f

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