Theorems · Theorem · field theory

Subfield.relrank_comap

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

Defined in

Mathlib.FieldTheory.Relrank

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldField