Theorems · Theorem · field theory

IntermediateField.adjoin_algHom_ext

∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Semiring K] [inst_4 : Algebra F K] {s : Set E} ⦃φ₁ φ₂ : ↥(IntermediateField.adjoin F s) →ₐ[F] K⦄,
  (∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩) → φ₁ = φ₂

Defined in

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraSemiringAlgebra