lift_relrank_comap — Mathlib

English

For f: L →ₐ[F] E, the lifted relrank of (A.comap f) with B equals the lifted relrank of A with B.map f.

Русский

Для f: L →ₐ[F] E, поднятое relrank (A.comap f) с B равно поднятому relrank(A, B.map f).

LaTeX

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

Lean4

theorem lift_relrank_comap (f : L →ₐ[F] E) (B : IntermediateField F L) :
    Cardinal.lift.{v} (relrank (A.comap f) B) = Cardinal.lift.{w} (relrank A (B.map f)) :=
  A.toSubfield.lift_relrank_comap f.toRingHom B.toSubfield

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