relrank_map_map — Mathlib

English

Relrank is preserved under the map operation: relrank(A.map f, B.map f) = relrank(A,B).

Русский

Relrank сохраняется под отображением: relrank(A.map f, B.map f) = relrank(A,B).

LaTeX

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

Lean4

theorem relrank_map_map {L : Type v} [Field L] [Algebra F L] (f : E →ₐ[F] L) :
    relrank (A.map f) (B.map f) = relrank A B := by simpa only [lift_id] using lift_relrank_map_map A B f

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