# mathlib3documentation

field_theory.subfield

# Subfields #

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

Let `K` be a field. This file defines the "bundled" subfield type `subfield K`, a type whose terms correspond to subfields of `K`. This is the preferred way to talk about subfields in mathlib. Unbundled subfields (`s : set K` and `is_subfield s`) are not in this file, and they will ultimately be deprecated.

We prove that subfields are a complete lattice, and that you can `map` (pushforward) and `comap` (pull back) them along ring homomorphisms.

We define the `closure` construction from `set R` to `subfield R`, sending a subset of `R` to the subfield it generates, and prove that it is a Galois insertion.

## Main definitions #

Notation used here:

`(K : Type u) [field K] (L : Type u) [field L] (f g : K →+* L)` `(A : subfield K) (B : subfield L) (s : set K)`

• `subfield R` : the type of subfields of a ring `R`.

• `instance : complete_lattice (subfield R)` : the complete lattice structure on the subfields.

• `subfield.closure` : subfield closure of a set, i.e., the smallest subfield that includes the set.

• `subfield.gi` : `closure : set M → subfield M` and coercion `coe : subfield M → set M` form a `galois_insertion`.

• `comap f B : subfield K` : the preimage of a subfield `B` along the ring homomorphism `f`

• `map f A : subfield L` : the image of a subfield `A` along the ring homomorphism `f`.

• `prod A B : subfield (K × L)` : the product of subfields

• `f.field_range : subfield B` : the range of the ring homomorphism `f`.

• `eq_locus_field f g : subfield K` : given ring homomorphisms `f g : K →+* R`, the subfield of `K` where `f x = g x`

## Implementation notes #

A subfield is implemented as a subring which is is closed under `⁻¹`.

Lattice inclusion (e.g. `≤` and `⊓`) is used rather than set notation (`⊆` and `∩`), although `∈` is defined as membership of a subfield's underlying set.

## Tags #

subfield, subfields

@[class]
structure subfield_class (S : Type u_1) (K : Type u_2) [field K] [ K] :
Prop
• to_subring_class :
• to_inv_mem_class :

`subfield_class S K` states `S` is a type of subsets `s ⊆ K` closed under field operations.

Instances of this typeclass
@[protected, instance]
def subfield_class.subfield_class.to_subgroup_class {K : Type u} [field K] (S : Type u_1) [ K] [h : K] :

A subfield contains `1`, products and inverses.

Be assured that we're not actually proving that subfields are subgroups: `subgroup_class` is really an abbreviation of `subgroup_with_or_without_zero_class`.

theorem subfield_class.coe_rat_mem {K : Type u} [field K] {S : Type u_1} [ K] [h : K] (s : S) (x : ) :
x s
@[protected, instance]
def subfield_class.has_rat_cast {K : Type u} [field K] {S : Type u_1} [ K] [h : K] (s : S) :
Equations
@[simp]
theorem subfield_class.coe_rat_cast {K : Type u} [field K] {S : Type u_1} [ K] [h : K] (s : S) (x : ) :
theorem subfield_class.rat_smul_mem {K : Type u} [field K] {S : Type u_1} [ K] [h : K] (s : S) (a : ) (x : s) :
a x s
@[protected, instance]
def subfield_class.has_smul {K : Type u} [field K] {S : Type u_1} [ K] [h : K] (s : S) :
Equations
@[simp]
theorem subfield_class.coe_rat_smul {K : Type u} [field K] {S : Type u_1} [ K] [h : K] (s : S) (a : ) (x : s) :
(a x) = a x
@[protected, instance]
def subfield_class.to_field {K : Type u} [field K] (S : Type u_1) [ K] [h : K] (s : S) :

A subfield inherits a field structure

Equations
• = _ _ _ _ _ _ _ _ _ _ _ _ _ _
@[protected, instance]
def subfield_class.to_linear_ordered_field (S : Type u_1) {K : Type u_2} [ K] [ K] (s : S) :

A subfield of a `linear_ordered_field` is a `linear_ordered_field`.

Equations
• = _ _ _ _ _ _ _ _ _ _ _ _ _ _
def subfield.to_subring {K : Type u} [field K] (self : subfield K) :

Reinterpret a `subfield` as a `subring`.

Instances for `subfield.to_subring`
structure subfield (K : Type u) [field K] :

`subfield R` is the type of subfields of `R`. A subfield of `R` is a subset `s` that is a multiplicative submonoid and an additive subgroup. Note in particular that it shares the same 0 and 1 as R.

Instances for `subfield`
def subfield.to_add_subgroup {K : Type u} [field K] (s : subfield K) :

The underlying `add_subgroup` of a subfield.

Equations
def subfield.to_submonoid {K : Type u} [field K] (s : subfield K) :

The underlying submonoid of a subfield.

Equations
@[protected, instance]
def subfield.set_like {K : Type u} [field K] :
Equations
@[protected, instance]
def subfield.subfield_class {K : Type u} [field K] :
K
@[simp]
theorem subfield.mem_carrier {K : Type u} [field K] {s : subfield K} {x : K} :
x s.carrier x s
@[simp]
theorem subfield.mem_mk {K : Type u} [field K] {S : set K} {x : K} (h₁ : {a b : K}, a S b S a * b S) (h₂ : 1 S) (h₃ : {a b : K}, a S b S a + b S) (h₄ : 0 S) (h₅ : {x : K}, x S -x S) (h₆ : (x : K), x S x⁻¹ S) :
x {carrier := S, mul_mem' := h₁, one_mem' := h₂, add_mem' := h₃, zero_mem' := h₄, neg_mem' := h₅, inv_mem' := h₆} x S
@[simp]
theorem subfield.coe_set_mk {K : Type u} [field K] (S : set K) (h₁ : {a b : K}, a S b S a * b S) (h₂ : 1 S) (h₃ : {a b : K}, a S b S a + b S) (h₄ : 0 S) (h₅ : {x : K}, x S -x S) (h₆ : (x : K), x S x⁻¹ S) :
{carrier := S, mul_mem' := h₁, one_mem' := h₂, add_mem' := h₃, zero_mem' := h₄, neg_mem' := h₅, inv_mem' := h₆} = S
@[simp]
theorem subfield.mk_le_mk {K : Type u} [field K] {S S' : set K} (h₁ : {a b : K}, a S b S a * b S) (h₂ : 1 S) (h₃ : {a b : K}, a S b S a + b S) (h₄ : 0 S) (h₅ : {x : K}, x S -x S) (h₆ : (x : K), x S x⁻¹ S) (h₁' : {a b : K}, a S' b S' a * b S') (h₂' : 1 S') (h₃' : {a b : K}, a S' b S' a + b S') (h₄' : 0 S') (h₅' : {x : K}, x S' -x S') (h₆' : (x : K), x S' x⁻¹ S') :
{carrier := S, mul_mem' := h₁, one_mem' := h₂, add_mem' := h₃, zero_mem' := h₄, neg_mem' := h₅, inv_mem' := h₆} {carrier := S', mul_mem' := h₁', one_mem' := h₂', add_mem' := h₃', zero_mem' := h₄', neg_mem' := h₅', inv_mem' := h₆'} S S'
@[ext]
theorem subfield.ext {K : Type u} [field K] {S T : subfield K} (h : (x : K), x S x T) :
S = T

Two subfields are equal if they have the same elements.

@[protected]
def subfield.copy {K : Type u} [field K] (S : subfield K) (s : set K) (hs : s = S) :

Copy of a subfield with a new `carrier` equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem subfield.coe_copy {K : Type u} [field K] (S : subfield K) (s : set K) (hs : s = S) :
(S.copy s hs) = s
theorem subfield.copy_eq {K : Type u} [field K] (S : subfield K) (s : set K) (hs : s = S) :
S.copy s hs = S
@[simp]
theorem subfield.coe_to_subring {K : Type u} [field K] (s : subfield K) :
@[simp]
theorem subfield.mem_to_subring {K : Type u} [field K] (s : subfield K) (x : K) :
def subring.to_subfield {K : Type u} [field K] (s : subring K) (hinv : (x : K), x s x⁻¹ s) :

A `subring` containing inverses is a `subfield`.

Equations
@[protected]
theorem subfield.one_mem {K : Type u} [field K] (s : subfield K) :
1 s

A subfield contains the field's 1.

@[protected]
theorem subfield.zero_mem {K : Type u} [field K] (s : subfield K) :
0 s

A subfield contains the field's 0.

@[protected]
theorem subfield.mul_mem {K : Type u} [field K] (s : subfield K) {x y : K} :
x s y s x * y s

A subfield is closed under multiplication.

@[protected]
theorem subfield.add_mem {K : Type u} [field K] (s : subfield K) {x y : K} :
x s y s x + y s

A subfield is closed under addition.

@[protected]
theorem subfield.neg_mem {K : Type u} [field K] (s : subfield K) {x : K} :
x s -x s

A subfield is closed under negation.

@[protected]
theorem subfield.sub_mem {K : Type u} [field K] (s : subfield K) {x y : K} :
x s y s x - y s

A subfield is closed under subtraction.

@[protected]
theorem subfield.inv_mem {K : Type u} [field K] (s : subfield K) {x : K} :
x s x⁻¹ s

A subfield is closed under inverses.

@[protected]
theorem subfield.div_mem {K : Type u} [field K] (s : subfield K) {x y : K} :
x s y s x / y s

A subfield is closed under division.

@[protected]
theorem subfield.list_prod_mem {K : Type u} [field K] (s : subfield K) {l : list K} :
( (x : K), x l x s) l.prod s

Product of a list of elements in a subfield is in the subfield.

@[protected]
theorem subfield.list_sum_mem {K : Type u} [field K] (s : subfield K) {l : list K} :
( (x : K), x l x s) l.sum s

Sum of a list of elements in a subfield is in the subfield.

@[protected]
theorem subfield.multiset_prod_mem {K : Type u} [field K] (s : subfield K) (m : multiset K) :
( (a : K), a m a s) m.prod s

Product of a multiset of elements in a subfield is in the subfield.

@[protected]
theorem subfield.multiset_sum_mem {K : Type u} [field K] (s : subfield K) (m : multiset K) :
( (a : K), a m a s) m.sum s

Sum of a multiset of elements in a `subfield` is in the `subfield`.

@[protected]
theorem subfield.prod_mem {K : Type u} [field K] (s : subfield K) {ι : Type u_1} {t : finset ι} {f : ι K} (h : (c : ι), c t f c s) :
t.prod (λ (i : ι), f i) s

Product of elements of a subfield indexed by a `finset` is in the subfield.

@[protected]
theorem subfield.sum_mem {K : Type u} [field K] (s : subfield K) {ι : Type u_1} {t : finset ι} {f : ι K} (h : (c : ι), c t f c s) :
t.sum (λ (i : ι), f i) s

Sum of elements in a `subfield` indexed by a `finset` is in the `subfield`.

@[protected]
theorem subfield.pow_mem {K : Type u} [field K] (s : subfield K) {x : K} (hx : x s) (n : ) :
x ^ n s
@[protected]
theorem subfield.zsmul_mem {K : Type u} [field K] (s : subfield K) {x : K} (hx : x s) (n : ) :
n x s
@[protected]
theorem subfield.coe_int_mem {K : Type u} [field K] (s : subfield K) (n : ) :
n s
theorem subfield.zpow_mem {K : Type u} [field K] (s : subfield K) {x : K} (hx : x s) (n : ) :
x ^ n s
@[protected, instance]
def subfield.ring {K : Type u} [field K] (s : subfield K) :
Equations
@[protected, instance]
def subfield.has_div {K : Type u} [field K] (s : subfield K) :
Equations
@[protected, instance]
def subfield.has_inv {K : Type u} [field K] (s : subfield K) :
Equations
@[protected, instance]
def subfield.int.has_pow {K : Type u} [field K] (s : subfield K) :
Equations
@[protected, instance]
def subfield.to_field {K : Type u} [field K] (s : subfield K) :

A subfield inherits a field structure

Equations
@[protected, instance]

A subfield of a `linear_ordered_field` is a `linear_ordered_field`.

Equations
@[simp, norm_cast]
theorem subfield.coe_add {K : Type u} [field K] (s : subfield K) (x y : s) :
(x + y) = x + y
@[simp, norm_cast]
theorem subfield.coe_sub {K : Type u} [field K] (s : subfield K) (x y : s) :
(x - y) = x - y
@[simp, norm_cast]
theorem subfield.coe_neg {K : Type u} [field K] (s : subfield K) (x : s) :
@[simp, norm_cast]
theorem subfield.coe_mul {K : Type u} [field K] (s : subfield K) (x y : s) :
(x * y) = x * y
@[simp, norm_cast]
theorem subfield.coe_div {K : Type u} [field K] (s : subfield K) (x y : s) :
(x / y) = x / y
@[simp, norm_cast]
theorem subfield.coe_inv {K : Type u} [field K] (s : subfield K) (x : s) :
@[simp, norm_cast]
theorem subfield.coe_zero {K : Type u} [field K] (s : subfield K) :
0 = 0
@[simp, norm_cast]
theorem subfield.coe_one {K : Type u} [field K] (s : subfield K) :
1 = 1
def subfield.subtype {K : Type u} [field K] (s : subfield K) :

The embedding from a subfield of the field `K` to `K`.

Equations
@[protected, instance]
def subfield.to_algebra {K : Type u} [field K] (s : subfield K) :
K
Equations
@[simp]
theorem subfield.coe_subtype {K : Type u} [field K] (s : subfield K) :

# Partial order #

@[simp]
theorem subfield.mem_to_submonoid {K : Type u} [field K] {s : subfield K} {x : K} :
x s
@[simp]
theorem subfield.coe_to_submonoid {K : Type u} [field K] (s : subfield K) :
@[simp]
theorem subfield.mem_to_add_subgroup {K : Type u} [field K] {s : subfield K} {x : K} :
x s
@[simp]

# top #

@[protected, instance]
def subfield.has_top {K : Type u} [field K] :

The subfield of `K` containing all elements of `K`.

Equations
@[protected, instance]
def subfield.inhabited {K : Type u} [field K] :
Equations
@[simp]
theorem subfield.mem_top {K : Type u} [field K] (x : K) :
@[simp]
theorem subfield.coe_top {K : Type u} [field K] :
@[simp]
theorem subfield.top_equiv_apply {K : Type u} [field K] (r : ) :
def subfield.top_equiv {K : Type u} [field K] :

The ring equiv between the top element of `subfield K` and `K`.

Equations
@[simp]

# comap #

def subfield.comap {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) (s : subfield L) :

The preimage of a subfield along a ring homomorphism is a subfield.

Equations
@[simp]
theorem subfield.coe_comap {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) (s : subfield L) :
@[simp]
theorem subfield.mem_comap {K : Type u} {L : Type v} [field K] [field L] {s : subfield L} {f : K →+* L} {x : K} :
x f x s
theorem subfield.comap_comap {K : Type u} {L : Type v} {M : Type w} [field K] [field L] [field M] (s : subfield M) (g : L →+* M) (f : K →+* L) :
s) = subfield.comap (g.comp f) s

# map #

def subfield.map {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) (s : subfield K) :

The image of a subfield along a ring homomorphism is a subfield.

Equations
@[simp]
theorem subfield.coe_map {K : Type u} {L : Type v} [field K] [field L] (s : subfield K) (f : K →+* L) :
s) = f '' s
@[simp]
theorem subfield.mem_map {K : Type u} {L : Type v} [field K] [field L] {f : K →+* L} {s : subfield K} {y : L} :
y s (x : K) (H : x s), f x = y
theorem subfield.map_map {K : Type u} {L : Type v} {M : Type w} [field K] [field L] [field M] (s : subfield K) (g : L →+* M) (f : K →+* L) :
s) = subfield.map (g.comp f) s
theorem subfield.map_le_iff_le_comap {K : Type u} {L : Type v} [field K] [field L] {f : K →+* L} {s : subfield K} {t : subfield L} :
s t s
theorem subfield.gc_map_comap {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) :

# range #

def ring_hom.field_range {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) :

The range of a ring homomorphism, as a subfield of the target. See Note [range copy pattern].

Equations
Instances for `↥ring_hom.field_range`
@[simp]
theorem ring_hom.coe_field_range {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) :
@[simp]
theorem ring_hom.mem_field_range {K : Type u} {L : Type v} [field K] [field L] {f : K →+* L} {y : L} :
y f.field_range (x : K), f x = y
theorem ring_hom.field_range_eq_map {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) :
theorem ring_hom.map_field_range {K : Type u} {L : Type v} {M : Type w} [field K] [field L] [field M] (g : L →+* M) (f : K →+* L) :
@[protected, instance]
def ring_hom.fintype_field_range {K : Type u} {L : Type v} [field K] [field L] [fintype K] [decidable_eq L] (f : K →+* L) :

The range of a morphism of fields is a fintype, if the domain is a fintype.

Note that this instance can cause a diamond with `subtype.fintype` if `L` is also a fintype.

Equations

# inf #

@[protected, instance]
def subfield.has_inf {K : Type u} [field K] :

The inf of two subfields is their intersection.

Equations
@[simp]
theorem subfield.coe_inf {K : Type u} [field K] (p p' : subfield K) :
(p p') = p p'
@[simp]
theorem subfield.mem_inf {K : Type u} [field K] {p p' : subfield K} {x : K} :
x p p' x p x p'
@[protected, instance]
def subfield.has_Inf {K : Type u} [field K] :
Equations
@[simp, norm_cast]
theorem subfield.coe_Inf {K : Type u} [field K] (S : set (subfield K)) :
(has_Inf.Inf S) = (s : subfield K) (H : s S), s
theorem subfield.mem_Inf {K : Type u} [field K] {S : set (subfield K)} {x : K} :
x (p : subfield K), p S x p
@[simp]
theorem subfield.Inf_to_subring {K : Type u} [field K] (s : set (subfield K)) :
= (t : subfield K) (H : t s), t.to_subring
theorem subfield.is_glb_Inf {K : Type u} [field K] (S : set (subfield K)) :
@[protected, instance]
def subfield.complete_lattice {K : Type u} [field K] :

Subfields of a ring form a complete lattice.

Equations

# subfield closure of a subset #

def subfield.closure {K : Type u} [field K] (s : set K) :

The `subfield` generated by a set.

Equations
theorem subfield.mem_closure_iff {K : Type u} [field K] {s : set K} {x : K} :
(y : K) (H : y (z : K) (H : z , y / z = x
theorem subfield.subring_closure_le {K : Type u} [field K] (s : set K) :
@[simp]
theorem subfield.subset_closure {K : Type u} [field K] {s : set K} :
s

The subfield generated by a set includes the set.

theorem subfield.not_mem_of_not_mem_closure {K : Type u} [field K] {s : set K} {P : K} (hP : P ) :
P s
theorem subfield.mem_closure {K : Type u} [field K] {x : K} {s : set K} :
(S : subfield K), s S x S
@[simp]
theorem subfield.closure_le {K : Type u} [field K] {s : set K} {t : subfield K} :
s t

A subfield `t` includes `closure s` if and only if it includes `s`.

theorem subfield.closure_mono {K : Type u} [field K] ⦃s t : set K⦄ (h : s t) :

Subfield closure of a set is monotone in its argument: if `s ⊆ t`, then `closure s ≤ closure t`.

theorem subfield.closure_eq_of_le {K : Type u} [field K] {s : set K} {t : subfield K} (h₁ : s t) (h₂ : t ) :
theorem subfield.closure_induction {K : Type u} [field K] {s : set K} {p : K Prop} {x : K} (h : x ) (Hs : (x : K), x s p x) (H1 : p 1) (Hadd : (x y : K), p x p y p (x + y)) (Hneg : (x : K), p x p (-x)) (Hinv : (x : K), p x p x⁻¹) (Hmul : (x y : K), p x p y p (x * y)) :
p x

An induction principle for closure membership. If `p` holds for `1`, and all elements of `s`, and is preserved under addition, negation, and multiplication, then `p` holds for all elements of the closure of `s`.

@[protected]
def subfield.gi (K : Type u) [field K] :

`closure` forms a Galois insertion with the coercion to set.

Equations
theorem subfield.closure_eq {K : Type u} [field K] (s : subfield K) :

Closure of a subfield `S` equals `S`.

@[simp]
theorem subfield.closure_empty {K : Type u} [field K] :
@[simp]
theorem subfield.closure_univ {K : Type u} [field K] :
theorem subfield.closure_union {K : Type u} [field K] (s t : set K) :
theorem subfield.closure_Union {K : Type u} [field K] {ι : Sort u_1} (s : ι set K) :
subfield.closure ( (i : ι), s i) = (i : ι), subfield.closure (s i)
theorem subfield.closure_sUnion {K : Type u} [field K] (s : set (set K)) :
= (t : set K) (H : t s),
theorem subfield.map_sup {K : Type u} {L : Type v} [field K] [field L] (s t : subfield K) (f : K →+* L) :
(s t) = s t
theorem subfield.map_supr {K : Type u} {L : Type v} [field K] [field L] {ι : Sort u_1} (f : K →+* L) (s : ι ) :
(supr s) = (i : ι), (s i)
theorem subfield.comap_inf {K : Type u} {L : Type v} [field K] [field L] (s t : subfield L) (f : K →+* L) :
(s t) =
theorem subfield.comap_infi {K : Type u} {L : Type v} [field K] [field L] {ι : Sort u_1} (f : K →+* L) (s : ι ) :
(infi s) = (i : ι), (s i)
@[simp]
theorem subfield.map_bot {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) :
@[simp]
theorem subfield.comap_top {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) :
theorem subfield.mem_supr_of_directed {K : Type u} [field K] {ι : Sort u_1} [hι : nonempty ι] {S : ι } (hS : S) {x : K} :
(x (i : ι), S i) (i : ι), x S i

The underlying set of a non-empty directed Sup of subfields is just a union of the subfields. Note that this fails without the directedness assumption (the union of two subfields is typically not a subfield)

theorem subfield.coe_supr_of_directed {K : Type u} [field K] {ι : Sort u_1} [hι : nonempty ι] {S : ι } (hS : S) :
( (i : ι), S i) = (i : ι), (S i)
theorem subfield.mem_Sup_of_directed_on {K : Type u} [field K] {S : set (subfield K)} (Sne : S.nonempty) (hS : S) {x : K} :
x (s : subfield K) (H : s S), x s
theorem subfield.coe_Sup_of_directed_on {K : Type u} [field K] {S : set (subfield K)} (Sne : S.nonempty) (hS : S) :
(has_Sup.Sup S) = (s : subfield K) (H : s S), s
def ring_hom.range_restrict_field {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) :

Restriction of a ring homomorphism to its range interpreted as a subfield.

Equations
@[simp]
theorem ring_hom.coe_range_restrict_field {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) (x : K) :
def ring_hom.eq_locus_field {K : Type u} {L : Type v} [field K] [field L] (f g : K →+* L) :

The subfield of elements `x : R` such that `f x = g x`, i.e., the equalizer of f and g as a subfield of R

Equations
theorem ring_hom.eq_on_field_closure {K : Type u} {L : Type v} [field K] [field L] {f g : K →+* L} {s : set K} (h : g s) :
g

If two ring homomorphisms are equal on a set, then they are equal on its subfield closure.

theorem ring_hom.eq_of_eq_on_subfield_top {K : Type u} {L : Type v} [field K] [field L] {f g : K →+* L} (h : g ) :
f = g
theorem ring_hom.eq_of_eq_on_of_field_closure_eq_top {K : Type u} {L : Type v} [field K] [field L] {s : set K} (hs : = ) {f g : K →+* L} (h : g s) :
f = g
theorem ring_hom.field_closure_preimage_le {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) (s : set L) :
theorem ring_hom.map_field_closure {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) (s : set K) :

The image under a ring homomorphism of the subfield generated by a set equals the subfield generated by the image of the set.

def subfield.inclusion {K : Type u} [field K] {S T : subfield K} (h : S T) :

The ring homomorphism associated to an inclusion of subfields.

Equations
@[simp]
theorem subfield.field_range_subtype {K : Type u} [field K] (s : subfield K) :
def ring_equiv.subfield_congr {K : Type u} [field K] {s t : subfield K} (h : s = t) :

Makes the identity isomorphism from a proof two subfields of a multiplicative monoid are equal.

Equations
theorem subfield.closure_preimage_le {K : Type u} {L : Type v} [field K] [field L] (f : K →+* L) (s : set L) :