Theorems · Theorem · field theory

Subfield.lift_relrank_comap

∀ {E : Type v} [inst : Field E] {L : Type w} [inst_1 : Field L] (A : Subfield E) (f : L →+* E) (B : Subfield L),
  Cardinal.lift.{v, w} ((Subfield.comap f A).relrank B) = Cardinal.lift.{w, v} (A.relrank (Subfield.map f B))

Defined in

Mathlib.FieldTheory.Relrank

Cited by

4 results in Mathlib

Foundations

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

Assumes

FieldField