Theorems · Theorem · field theory

Field.Emb.Cardinal.embFunctor.congr_simp

∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E]
  ⦃i j : WithTop (Module.rank F E).ord.ToType⦄ (h : i ≤ j)
  (f f_1 : ↥(Field.Emb.Cardinal.filtration j) →ₐ[F] AlgebraicClosure E),
  f = f_1 → Field.Emb.Cardinal.embFunctor F E h f = Field.Emb.Cardinal.embFunctor F E h f_1

Defined in

Mathlib.FieldTheory.CardinalEmb

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFactAlgebra.IsAlgebraic