Theorems · Definition · field theory

Field.embEquivOfEquiv

(F : Type u) →
  (E : Type v) →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          (K : Type w) → [inst_3 : Field K] → [inst_4 : Algebra F K] → (E ≃ₐ[F] K) → Field.Emb F E ≃ Field.Emb F K

A random bijection between Field.Emb F E and Field.Emb F K when E and K are isomorphic as F-algebras.

Defined in

Mathlib.FieldTheory.SeparableDegree

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFieldAlgebra