# Adjoining Elements to Fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we introduce the notion of adjoining elements to fields. This isn't quite the same as adjoining elements to rings. For example, `algebra.adjoin K {x}` might not include `x⁻¹`.

## Main results #

• `adjoin_adjoin_left`: adjoining S and then T is the same as adjoining `S ∪ T`.
• `bot_eq_top_of_rank_adjoin_eq_one`: if `F⟮x⟯` has dimension `1` over `F` for every `x` in `E` then `F = E`

## Notation #

• `F⟮α⟯`: adjoin a single element `α` to `F`.
def intermediate_field.adjoin (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (S : set E) :

`adjoin F S` extends a field `F` by adjoining a set `S ⊆ E`.

Equations
Instances for `↥intermediate_field.adjoin`
@[simp]
theorem intermediate_field.adjoin_le_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {S : set E} {T : E} :
S T
theorem intermediate_field.gc {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :
def intermediate_field.gi {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :

Galois insertion between `adjoin` and `coe`.

Equations
@[protected, instance]
def intermediate_field.complete_lattice {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :
Equations
@[protected, instance]
def intermediate_field.inhabited {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :
Equations
theorem intermediate_field.coe_bot {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :
theorem intermediate_field.mem_bot {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {x : E} :
@[simp]
theorem intermediate_field.bot_to_subalgebra {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :
@[simp]
theorem intermediate_field.coe_top {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :
@[simp]
theorem intermediate_field.mem_top {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {x : E} :
@[simp]
theorem intermediate_field.top_to_subalgebra {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :
@[simp]
theorem intermediate_field.top_to_subfield {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :
@[simp, norm_cast]
theorem intermediate_field.coe_inf {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (S T : E) :
(S T) = S T
@[simp]
theorem intermediate_field.mem_inf {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {S T : E} {x : E} :
x S T x S x T
@[simp]
theorem intermediate_field.inf_to_subalgebra {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (S T : E) :
@[simp]
theorem intermediate_field.inf_to_subfield {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (S T : E) :
@[simp, norm_cast]
theorem intermediate_field.coe_Inf {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (S : set E)) :
@[simp]
theorem intermediate_field.Inf_to_subalgebra {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (S : set E)) :
@[simp]
theorem intermediate_field.Inf_to_subfield {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (S : set E)) :
@[simp, norm_cast]
theorem intermediate_field.coe_infi {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {ι : Sort u_3} (S : ι ) :
(infi S) = (i : ι), (S i)
@[simp]
theorem intermediate_field.infi_to_subalgebra {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {ι : Sort u_3} (S : ι ) :
@[simp]
theorem intermediate_field.infi_to_subfield {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {ι : Sort u_3} (S : ι ) :
(infi S).to_subfield = (i : ι), (S i).to_subfield
@[simp]
theorem intermediate_field.equiv_of_eq_apply {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {S T : E} (h : S = T) (x : S) :
= x, _⟩
def intermediate_field.equiv_of_eq {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {S T : E} (h : S = T) :

Construct an algebra isomorphism from an equality of intermediate fields

Equations
@[simp]
theorem intermediate_field.equiv_of_eq_symm {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {S T : E} (h : S = T) :
@[simp]
theorem intermediate_field.equiv_of_eq_rfl {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (S : E) :
@[simp]
theorem intermediate_field.equiv_of_eq_trans {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {S T U : E} (hST : S = T) (hTU : T = U) :
noncomputable def intermediate_field.bot_equiv (F : Type u_1) [field F] (E : Type u_2) [field E] [ E] :

The bottom intermediate_field is isomorphic to the field.

Equations
@[simp]
theorem intermediate_field.bot_equiv_def {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (x : F) :
( ) x) = x
@[simp]
theorem intermediate_field.bot_equiv_symm {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (x : F) :
@[protected, instance]
noncomputable def intermediate_field.algebra_over_bot {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :
Equations
theorem intermediate_field.coe_algebra_map_over_bot {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :
F) =
@[protected, instance]
def intermediate_field.is_scalar_tower_over_bot {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :
@[simp]
theorem intermediate_field.top_equiv_apply {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (ᾰ : (.to_subalgebra)) :
def intermediate_field.top_equiv {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :

The top intermediate_field is isomorphic to the field.

This is the intermediate field version of `subalgebra.top_equiv`.

Equations
@[simp]
theorem intermediate_field.top_equiv_symm_apply_coe {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (a : E) :
@[simp]
theorem intermediate_field.restrict_scalars_bot_eq_self {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (K : E) :
@[simp]
theorem intermediate_field.restrict_scalars_top {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {K : Type u_3} [field K] [ E] [ F] [ E] :
theorem alg_hom.field_range_eq_map {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {K : Type u_3} [field K] [ K] (f : E →ₐ[F] K) :
theorem alg_hom.map_field_range {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {K : Type u_3} {L : Type u_4} [field K] [field L] [ K] [ L] (f : E →ₐ[F] K) (g : K →ₐ[F] L) :
theorem alg_hom.field_range_eq_top {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {K : Type u_3} [field K] [ K] {f : E →ₐ[F] K} :
@[simp]
theorem alg_equiv.field_range_eq_top {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {K : Type u_3} [field K] [ K] (f : E ≃ₐ[F] K) :
theorem intermediate_field.adjoin_eq_range_algebra_map_adjoin (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (S : set E) :
theorem intermediate_field.adjoin.algebra_map_mem (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (S : set E) (x : F) :
E) x
theorem intermediate_field.adjoin.range_algebra_map_subset (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (S : set E) :
@[protected, instance]
def intermediate_field.adjoin.field_coe (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (S : set E) :
Equations
theorem intermediate_field.subset_adjoin (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (S : set E) :
S
@[protected, instance]
def intermediate_field.adjoin.set_coe (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (S : set E) :
Equations
theorem intermediate_field.adjoin.mono (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (S T : set E) (h : S T) :
theorem intermediate_field.subset_adjoin_of_subset_left {E : Type u_2} [field E] (S : set E) {F : subfield E} {T : set E} (HT : T F) :
T
theorem intermediate_field.subset_adjoin_of_subset_right (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (S : set E) {T : set E} (H : T S) :
T
@[simp]
theorem intermediate_field.adjoin_empty (F : Type u_1) (E : Type u_2) [field F] [field E] [ E] :
@[simp]
theorem intermediate_field.adjoin_univ (F : Type u_1) (E : Type u_2) [field F] [field E] [ E] :
theorem intermediate_field.adjoin_le_subfield (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (S : set E) {K : subfield E} (HF : set.range E) K) (HS : S K) :

If `K` is a field with `F ⊆ K` and `S ⊆ K` then `adjoin F S ≤ K`.

theorem intermediate_field.adjoin_subset_adjoin_iff (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] {F' : Type u_3} [field F'] [algebra F' E] {S S' : set E} :
S') set.range E) S') S S')
theorem intermediate_field.adjoin_adjoin_left (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (S T : set E) :

`F[S][T] = F[S ∪ T]`

@[simp]
theorem intermediate_field.adjoin_insert_adjoin (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (S : set E) (x : E) :
theorem intermediate_field.adjoin_adjoin_comm (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (S T : set E) :

`F[S][T] = F[T][S]`

theorem intermediate_field.adjoin_map (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (S : set E) {E' : Type u_3} [field E'] [ E'] (f : E →ₐ[F] E') :
theorem intermediate_field.algebra_adjoin_le_adjoin (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (S : set E) :
theorem intermediate_field.adjoin_eq_algebra_adjoin (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (S : set E) (inv_mem : (x : E), x x⁻¹ ) :
theorem intermediate_field.eq_adjoin_of_eq_algebra_adjoin (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (S : set E) (K : E) (h : K.to_subalgebra = ) :
theorem intermediate_field.adjoin_induction (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] {s : set E} {p : E Prop} {x : E} (h : x ) (Hs : (x : E), x s p x) (Hmap : (x : F), p ( E) x)) (Hadd : (x y : E), p x p y p (x + y)) (Hneg : (x : E), p x p (-x)) (Hinv : (x : E), p x p x⁻¹) (Hmul : (x y : E), p x p y p (x * y)) :
p x
@[class]
structure intermediate_field.insert {α : Type u_3} (s : set α) :
Type u_3

Variation on `set.insert` to enable good notation for adjoining elements to fields. Used to preferentially use `singleton` rather than `insert` when adjoining one element.

Instances of this typeclass
Instances of other typeclasses for `intermediate_field.insert`
• intermediate_field.insert.has_sizeof_inst
@[protected, instance]
Equations
@[protected, instance]
def intermediate_field.insert_nonempty {α : Type u_1} (s : set α) :
Equations
theorem intermediate_field.mem_adjoin_simple_self (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (α : E) :
α Fα
def intermediate_field.adjoin_simple.gen (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (α : E) :

generator of `F⟮α⟯`

Equations
@[simp]
theorem intermediate_field.adjoin_simple.algebra_map_gen (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (α : E) :
E) = α
@[simp]
theorem intermediate_field.adjoin_simple.is_integral_gen (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (α : E) :
theorem intermediate_field.adjoin_simple_adjoin_simple (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (α β : E) :
= Fα, β
theorem intermediate_field.adjoin_simple_comm (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (α β : E) :
theorem intermediate_field.adjoin_algebraic_to_subalgebra {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {S : set E} (hS : (x : E), x S x) :
theorem intermediate_field.adjoin_simple_to_subalgebra_of_integral {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {α : E} (hα : α) :
theorem intermediate_field.is_splitting_field_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {p : polynomial F} {K : E} :
p K =
theorem intermediate_field.adjoin_root_set_is_splitting_field {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {p : polynomial F} (hp : p) :
theorem intermediate_field.is_splitting_field_supr {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {ι : Type u_3} {t : ι } {p : ι } {s : finset ι} (h0 : s.prod (λ (i : ι), p i) 0) (h : (i : ι), i s (p i)) :
( (i : ι) (H : i s), t i) (s.prod (λ (i : ι), p i))

A compositum of splitting fields is a splitting field

@[simp]
theorem intermediate_field.adjoin_simple_le_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {α : E} {K : E} :
Fα K α K
theorem intermediate_field.adjoin_simple_is_compact_element {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (x : E) :

Adjoining a single element is compact in the lattice of intermediate fields.

theorem intermediate_field.adjoin_finset_is_compact_element {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (S : finset E) :

Adjoining a finite subset is compact in the lattice of intermediate fields.

theorem intermediate_field.adjoin_finite_is_compact_element {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {S : set E} (h : S.finite) :

Adjoining a finite subset is compact in the lattice of intermediate fields.

@[protected, instance]
def intermediate_field.is_compactly_generated {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :

The lattice of intermediate fields is compactly generated.

theorem intermediate_field.exists_finset_of_mem_supr {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {ι : Type u_3} {f : ι } {x : E} (hx : x (i : ι), f i) :
(s : finset ι), x (i : ι) (H : i s), f i
theorem intermediate_field.exists_finset_of_mem_supr' {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {ι : Type u_3} {f : ι } {x : E} (hx : x (i : ι), f i) :
(s : finset (Σ (i : ι), (f i))), x (i : Σ (i : ι), (f i)) (H : i s), F(i.snd)
theorem intermediate_field.exists_finset_of_mem_supr'' {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {ι : Type u_3} {f : ι } (h : (i : ι), (f i)) {x : E} (hx : x (i : ι), f i) :
(s : finset (Σ (i : ι), (f i))), x (i : Σ (i : ι), (f i)) (H : i s), ((minpoly F i.snd).root_set E)
@[simp]
theorem intermediate_field.adjoin_eq_bot_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {S : set E} :
@[simp]
theorem intermediate_field.adjoin_simple_eq_bot_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {α : E} :
@[simp]
theorem intermediate_field.adjoin_zero {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :
@[simp]
theorem intermediate_field.adjoin_one {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :
@[simp]
theorem intermediate_field.adjoin_int {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (n : ) :
@[simp]
theorem intermediate_field.adjoin_nat {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (n : ) :
@[simp]
theorem intermediate_field.rank_eq_one_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {K : E} :
K = 1 K =
@[simp]
theorem intermediate_field.finrank_eq_one_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {K : E} :
K =
@[simp]
theorem intermediate_field.rank_bot {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :
= 1
@[simp]
theorem intermediate_field.finrank_bot {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :
theorem intermediate_field.rank_adjoin_eq_one_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {S : set E} :
theorem intermediate_field.rank_adjoin_simple_eq_one_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {α : E} :
Fα = 1 α
theorem intermediate_field.finrank_adjoin_eq_one_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {S : set E} :
theorem intermediate_field.finrank_adjoin_simple_eq_one_iff {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {α : E} :
α
theorem intermediate_field.bot_eq_top_of_rank_adjoin_eq_one {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (h : (x : E), Fx = 1) :

If `F⟮x⟯` has dimension `1` over `F` for every `x ∈ E` then `F = E`.

theorem intermediate_field.bot_eq_top_of_finrank_adjoin_eq_one {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (h : (x : E), ) :
theorem intermediate_field.subsingleton_of_rank_adjoin_eq_one {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (h : (x : E), Fx = 1) :
theorem intermediate_field.subsingleton_of_finrank_adjoin_eq_one {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (h : (x : E), ) :
theorem intermediate_field.bot_eq_top_of_finrank_adjoin_le_one {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] [ E] (h : (x : E), ) :

If `F⟮x⟯` has dimension `≤1` over `F` for every `x ∈ E` then `F = E`.

theorem intermediate_field.subsingleton_of_finrank_adjoin_le_one {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] [ E] (h : (x : E), ) :
theorem intermediate_field.minpoly_gen {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {α : E} (h : α) :
= α
theorem intermediate_field.aeval_gen_minpoly (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] (α : E) :
(minpoly F α) = 0
noncomputable def intermediate_field.adjoin_root_equiv_adjoin (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] {α : E} (h : α) :

algebra isomorphism between `adjoin_root` and `F⟮α⟯`

Equations
theorem intermediate_field.adjoin_root_equiv_adjoin_apply_root (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] {α : E} (h : α) :
noncomputable def intermediate_field.power_basis_aux {K : Type u_3} [field K] {L : Type u_4} [field L] [ L] {x : L} (hx : x) :

The elements `1, x, ..., x ^ (d - 1)` form a basis for `K⟮x⟯`, where `d` is the degree of the minimal polynomial of `x`.

Equations
@[simp]
theorem intermediate_field.adjoin.power_basis_dim {K : Type u_3} [field K] {L : Type u_4} [field L] [ L] {x : L} (hx : x) :
noncomputable def intermediate_field.adjoin.power_basis {K : Type u_3} [field K] {L : Type u_4} [field L] [ L] {x : L} (hx : x) :

The power basis `1, x, ..., x ^ (d - 1)` for `K⟮x⟯`, where `d` is the degree of the minimal polynomial of `x`.

Equations
@[simp]
theorem intermediate_field.adjoin.power_basis_gen {K : Type u_3} [field K] {L : Type u_4} [field L] [ L] {x : L} (hx : x) :
theorem intermediate_field.adjoin.finite_dimensional {K : Type u_3} [field K] {L : Type u_4} [field L] [ L] {x : L} (hx : x) :
theorem intermediate_field.adjoin.finrank {K : Type u_3} [field K] {L : Type u_4} [field L] [ L] {x : L} (hx : x) :
theorem minpoly.nat_degree_le {K : Type u_3} [field K] {L : Type u_4} [field L] [ L] {x : L} [ L] (hx : x) :
theorem minpoly.degree_le {K : Type u_3} [field K] {L : Type u_4} [field L] [ L] {x : L} [ L] (hx : x) :
noncomputable def intermediate_field.alg_hom_adjoin_integral_equiv (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] {α : E} {K : Type u_3} [field K] [ K] (h : α) :
(Fα →ₐ[F] K) {x // x (polynomial.map K) (minpoly F α)).roots}

Algebra homomorphism `F⟮α⟯ →ₐ[F] K` are in bijection with the set of roots of `minpoly α` in `K`.

Equations
noncomputable def intermediate_field.fintype_of_alg_hom_adjoin_integral (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] {α : E} {K : Type u_3} [field K] [ K] (h : α) :

Fintype of algebra homomorphism `F⟮α⟯ →ₐ[F] K`

Equations
theorem intermediate_field.card_alg_hom_adjoin_integral (F : Type u_1) [field F] {E : Type u_2} [field E] [ E] {α : E} {K : Type u_3} [field K] [ K] (h : α) (h_sep : (minpoly F α).separable) (h_splits : (minpoly F α)) :
def intermediate_field.fg {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (S : E) :
Prop

An intermediate field `S` is finitely generated if there exists `t : finset E` such that `intermediate_field.adjoin F t = S`.

Equations
theorem intermediate_field.fg_adjoin_finset {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (t : finset E) :
theorem intermediate_field.fg_def {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] {S : E} :
S.fg (t : set E), t.finite
theorem intermediate_field.fg_bot {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] :
theorem intermediate_field.fg_of_fg_to_subalgebra {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (S : E) (h : S.to_subalgebra.fg) :
S.fg
theorem intermediate_field.fg_of_noetherian {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (S : E) [ E] :
S.fg
theorem intermediate_field.induction_on_adjoin_finset {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (S : finset E) (P : Prop) (base : P ) (ih : (K : (x : E), x S P K P ) :
P
theorem intermediate_field.induction_on_adjoin_fg {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] (P : Prop) (base : P ) (ih : (K : (x : E), P K P ) (K : E) (hK : K.fg) :
P K
theorem intermediate_field.induction_on_adjoin {F : Type u_1} [field F] {E : Type u_2} [field E] [ E] [fd : E] (P : Prop) (base : P ) (ih : (K : (x : E), P K P ) (K : E) :
P K
def intermediate_field.lifts (F : Type u_1) (E : Type u_2) (K : Type u_3) [field F] [field E] [field K] [ E] [ K] :
Type (max u_2 u_3)

Lifts `L → K` of `F → K`

Equations
Instances for `intermediate_field.lifts`
@[protected, instance]
def intermediate_field.lifts.partial_order {F : Type u_1} {E : Type u_2} {K : Type u_3} [field F] [field E] [field K] [ E] [ K] :
Equations
@[protected, instance]
noncomputable def intermediate_field.lifts.order_bot {F : Type u_1} {E : Type u_2} {K : Type u_3} [field F] [field E] [field K] [ E] [ K] :
Equations
@[protected, instance]
noncomputable def intermediate_field.lifts.inhabited {F : Type u_1} {E : Type u_2} {K : Type u_3} [field F] [field E] [field K] [ E] [ K] :
Equations
theorem intermediate_field.lifts.eq_of_le {F : Type u_1} {E : Type u_2} {K : Type u_3} [field F] [field E] [field K] [ E] [ K] {x y : K} (hxy : x y) (s : (x.fst)) :
(x.snd) s = (y.snd) s, _⟩
theorem intermediate_field.lifts.exists_max_two {F : Type u_1} {E : Type u_2} {K : Type u_3} [field F] [field E] [field K] [ E] [ K] {c : set K)} {x y : K} (hc : c) (hx : x ) (hy : y ) :
(z : K), x z y z
theorem intermediate_field.lifts.exists_max_three {F : Type u_1} {E : Type u_2} {K : Type u_3} [field F] [field E] [field K] [ E] [ K] {c : set K)} {x y z : K} (hc : c) (hx : x ) (hy : y ) (hz : z ) :
(w : K), x w y w z w
def intermediate_field.lifts.upper_bound_intermediate_field {F : Type u_1} {E : Type u_2} {K : Type u_3} [field F] [field E] [field K] [ E] [ K] {c : set K)} (hc : c) :

An upper bound on a chain of lifts

Equations
noncomputable def intermediate_field.lifts.upper_bound_alg_hom {F : Type u_1} {E : Type u_2} {K : Type u_3} [field F] [field E] [field K] [ E] [ K] {c : set K)} (hc : c) :

The lift on the upper bound on a chain of lifts

Equations
noncomputable def intermediate_field.lifts.upper_bound {F : Type u_1} {E : Type u_2} {K : Type u_3} [field F] [field E] [field K] [ E] [ K] {c : set K)} (hc : c) :

An upper bound on a chain of lifts

Equations
theorem intermediate_field.lifts.exists_upper_bound {F : Type u_1} {E : Type u_2} {K : Type u_3} [field F] [field E] [field K] [ E] [ K] (c : set K)) (hc : c) :
(ub : K), (a : K), a c a ub
noncomputable def intermediate_field.lifts.lift_of_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [field F] [field E] [field K] [ E] [ K] (x : K) {s : E} (h1 : s) (h2 : (minpoly F s)) :

Extend a lift `x : lifts F E K` to an element `s : E` whose conjugates are all in `K`

Equations
theorem intermediate_field.lifts.le_lifts_of_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [field F] [field E] [field K] [ E] [ K] (x : K) {s : E} (h1 : s) (h2 : (minpoly F s)) :
theorem intermediate_field.lifts.mem_lifts_of_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [field F] [field E] [field K] [ E] [ K] (x : K) {s : E} (h1 : s) (h2 : (minpoly F s)) :
s (x.lift_of_splits h1 h2).fst
theorem intermediate_field.lifts.exists_lift_of_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [field F] [field E] [field K] [ E] [ K] (x : K) {s : E} (h1 : s) (h2 : (minpoly F s)) :
(y : K), x y s y.fst
theorem intermediate_field.alg_hom_mk_adjoin_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [field F] [field E] [field K] [ E] [ K] {S : set E} (hK : (s : E), s S s (minpoly F s)) :
theorem intermediate_field.alg_hom_mk_adjoin_splits' {F : Type u_1} {E : Type u_2} {K : Type u_3} [field F] [field E] [field K] [ E] [ K] {S : set E} (hS : = ) (hK : (x : E), x S x (minpoly F x)) :
theorem intermediate_field.le_sup_to_subalgebra {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (E1 E2 : L) :
theorem intermediate_field.sup_to_subalgebra {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (E1 E2 : L) [h1 : E1] [h2 : E2] :
@[protected, instance]
def intermediate_field.finite_dimensional_sup {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (E1 E2 : L) [h1 : E1] [h2 : E2] :
(E1 E2)
@[protected, instance]
def intermediate_field.finite_dimensional_supr_of_finite {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] {ι : Type u_3} {t : ι } [h : finite ι] [ (i : ι), (t i)] :
( (i : ι), t i)
@[protected, instance]
def intermediate_field.finite_dimensional_supr_of_finset {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] {ι : Type u_3} {f : ι } {s : finset ι} [h : (i : ι), i s (f i)] :
( (i : ι) (H : i s), f i)
theorem intermediate_field.is_algebraic_supr {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] {ι : Type u_3} {f : ι } (h : (i : ι), (f i)) :
( (i : ι), f i)

A compositum of algebraic extensions is algebraic

noncomputable def power_basis.equiv_adjoin_simple {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (pb : L) :

`pb.equiv_adjoin_simple` is the equivalence between `K⟮pb.gen⟯` and `L` itself.

Equations
@[simp]
theorem power_basis.equiv_adjoin_simple_aeval {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (pb : L) (f : polynomial K) :
@[simp]
theorem power_basis.equiv_adjoin_simple_gen {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (pb : L) :
= pb.gen
@[simp]
theorem power_basis.equiv_adjoin_simple_symm_aeval {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (pb : L) (f : polynomial K) :
@[simp]
theorem power_basis.equiv_adjoin_simple_symm_gen {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (pb : L) :