Theorems · Theorem · field theory

IntermediateField.lift_relrank_comap

∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type w} [inst_3 : Field L]
  [inst_4 : Algebra F L] (A : IntermediateField F E) (f : L →ₐ[F] E) (B : IntermediateField F L),
  Cardinal.lift.{v, w} ((IntermediateField.comap f A).relrank B) =
    Cardinal.lift.{w, v} (A.relrank (IntermediateField.map f B))

Defined in

Mathlib.FieldTheory.Relrank

Cited by

3 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraFieldAlgebra