Mathlib.Algebra.Field.Subfield.Defs

SubfieldClass structure

(S K : Type*) [DivisionRing K] [SetLike S K] : Prop
    extends SubringClass S K, InvMemClass S K

Full source

/-- `SubfieldClass S K` states `S` is a type of subsets `s ⊆ K` closed under field operations. -/
class SubfieldClass (S K : Type*) [DivisionRing K] [SetLike S K] : Prop
    extends SubringClass S K, InvMemClass S K

Subfield Class of a Division Ring

Informal description

A structure `SubfieldClass S K` asserts that `S` is a type of subsets of a division ring `K` that are closed under field operations. Specifically, it extends `SubringClass S K` (which ensures closure under addition, multiplication, and additive inverses) and `InvMemClass S K` (which ensures closure under multiplicative inverses for nonzero elements). This means that for any subset `s : S` of `K`, if `x, y ∈ s`, then `x + y ∈ s`, `x * y ∈ s`, `-x ∈ s`, and for any nonzero `x ∈ s`, `x⁻¹ ∈ s`. Additionally, the subset contains the multiplicative identity `1` and the additive identity `0`.

SubfieldClass.toSubgroupClass instance

: SubgroupClass S K

Full source

/-- A subfield contains `1`, products and inverses.

Be assured that we're not actually proving that subfields are subgroups:
`SubgroupClass` is really an abbreviation of `SubgroupWithOrWithoutZeroClass`.
-/
instance (priority := 100) toSubgroupClass : SubgroupClass S K :=
  { h with }

Subfields are Subgroups of the Multiplicative Group

Informal description

Every subfield of a division ring $K$ is also a subgroup of the multiplicative group of $K$.

SubfieldClass.nnratCast_mem theorem

(s : S) (q : ℚ≥0) : (q : K) ∈ s

Full source

@[aesop safe apply (rule_sets := [SetLike])]
lemma nnratCast_mem (s : S) (q : ℚ≥0) : (q : K) ∈ s := by
  simpa only [NNRat.cast_def] using div_mem (natCast_mem s q.num) (natCast_mem s q.den)

Nonnegative Rationals are Contained in Subfields

Informal description

For any subfield $s$ of a division ring $K$ and any nonnegative rational number $q$, the canonical image of $q$ in $K$ is an element of $s$.

SubfieldClass.ratCast_mem theorem

(s : S) (q : ℚ) : (q : K) ∈ s

Full source

@[aesop safe apply (rule_sets := [SetLike])]
lemma ratCast_mem (s : S) (q : ℚ) : (q : K) ∈ s := by
  simpa only [Rat.cast_def] using div_mem (intCast_mem s q.num) (natCast_mem s q.den)

Rational Numbers are Contained in Every Subfield

Informal description

For any subfield $s$ of a division ring $K$ and any rational number $q \in \mathbb{Q}$, the canonical image of $q$ in $K$ is an element of $s$.

SubfieldClass.instNNRatCast instance

(s : S) : NNRatCast s

Full source

instance instNNRatCast (s : S) : NNRatCast s where nnratCast q := ⟨q, nnratCast_mem s q⟩

Embedding of Nonnegative Rationals into Subfields

Informal description

For any subfield $s$ of a division ring $K$, the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ can be canonically embedded into $s$ via the natural inclusion map.

SubfieldClass.instRatCast instance

(s : S) : RatCast s

Full source

instance instRatCast (s : S) : RatCast s where ratCast q := ⟨q, ratCast_mem s q⟩

Rational Casting in Subfields

Informal description

For any subfield $s$ of a division ring $K$, $s$ has a canonical structure of a `RatCast`, meaning that rational numbers can be cast into $s$ in a way that is compatible with the embedding of $s$ into $K$.

SubfieldClass.coe_nnratCast theorem

(s : S) (q : ℚ≥0) : ((q : s) : K) = q

Full source

@[simp, norm_cast] lemma coe_nnratCast (s : S) (q : ℚ≥0) : ((q : s) : K) = q := rfl

Commutativity of Nonnegative Rational Embedding in Subfields

Informal description

For any subfield $s$ of a division ring $K$ and any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the canonical embedding of $q$ into $s$ followed by the inclusion map to $K$ equals $q$ itself. In other words, the diagram commutes: $$(q : s) \hookrightarrow K = q$$

SubfieldClass.coe_ratCast theorem

(s : S) (x : ℚ) : ((x : s) : K) = x

Full source

@[simp, norm_cast] lemma coe_ratCast (s : S) (x : ℚ) : ((x : s) : K) = x := rfl

Commutativity of Rational Casting in Subfields

Informal description

For any subfield $s$ of a division ring $K$ and any rational number $x \in \mathbb{Q}$, the canonical embedding of $x$ into $s$ followed by the inclusion map to $K$ equals $x$ itself. In other words, the diagram commutes: $\mathbb{Q} \to s \hookrightarrow K$ yields the original rational number $x$ when evaluated at $x$.

SubfieldClass.nnqsmul_mem theorem

(s : S) (q : ℚ≥0) (hx : x ∈ s) : q • x ∈ s

Full source

@[aesop safe apply (rule_sets := [SetLike])]
lemma nnqsmul_mem (s : S) (q : ℚ≥0) (hx : x ∈ s) : q • x ∈ s := by
  simpa only [NNRat.smul_def] using mul_mem (nnratCast_mem _ _) hx

Closure under nonnegative rational scalar multiplication in subfields

Informal description

Let $K$ be a division ring and $S$ be a subfield of $K$. For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$ and any element $x \in s$, the scalar multiple $q \cdot x$ belongs to $s$.

SubfieldClass.qsmul_mem theorem

(s : S) (q : ℚ) (hx : x ∈ s) : q • x ∈ s

Full source

@[aesop safe apply (rule_sets := [SetLike])]
lemma qsmul_mem (s : S) (q : ℚ) (hx : x ∈ s) : q • x ∈ s := by
  simpa only [Rat.smul_def] using mul_mem (ratCast_mem _ _) hx

Closure under Rational Scalar Multiplication in Subfields

Informal description

For any subfield $s$ of a division ring $K$ and any rational number $q \in \mathbb{Q}$, if an element $x$ belongs to $s$, then the scalar multiple $q \cdot x$ also belongs to $s$.

SubfieldClass.ofScientific_mem theorem

(s : S) {b : Bool} {n m : ℕ} : (OfScientific.ofScientific n b m : K) ∈ s

Full source

@[aesop safe apply (rule_sets := [SetLike])]
lemma ofScientific_mem (s : S) {b : Bool} {n m : ℕ} :
    (OfScientific.ofScientific n b m : K) ∈ s :=
  SubfieldClass.nnratCast_mem s (OfScientific.ofScientific n b m)

Subfields are closed under scientific notation elements

Informal description

For any subfield $s$ of a division ring $K$ and any natural numbers $n, m$ and boolean $b$, the element of $K$ represented in scientific notation as $\text{OfScientific.ofScientific}(n, b, m)$ is contained in $s$.

SubfieldClass.instSMulNNRat instance

(s : S) : SMul ℚ≥0 s

Full source

instance instSMulNNRat (s : S) : SMul ℚ≥0 s where smul q x := ⟨q • x, nnqsmul_mem s q x.2⟩

Scalar Multiplication by Nonnegative Rationals on Subfields

Informal description

For any subfield $s$ of a division ring $K$ (where $S$ is a type representing subfields of $K$), there is a scalar multiplication operation $\cdot$ defined between nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ and elements of $s$.

SubfieldClass.instSMulRat instance

(s : S) : SMul ℚ s

Full source

instance instSMulRat (s : S) : SMul ℚ s where smul q x := ⟨q • x, qsmul_mem s q x.2⟩

Scalar Multiplication by Rationals on Subfields

Informal description

For any subfield $s$ of a division ring $K$, there is a scalar multiplication operation $\cdot$ defined between rational numbers $\mathbb{Q}$ and elements of $s$.

SubfieldClass.coe_nnqsmul theorem

(s : S) (q : ℚ≥0) (x : s) : ↑(q • x) = q • (x : K)

Full source

@[simp, norm_cast] lemma coe_nnqsmul (s : S) (q : ℚ≥0) (x : s) : ↑(q • x) = q • (x : K) := rfl

Compatibility of Scalar Multiplication with Coercion for Nonnegative Rationals in Subfields

Informal description

For any subfield $s$ of a division ring $K$ and any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the scalar multiplication of $q$ with an element $x \in s$ is compatible with the coercion to $K$. That is, $\uparrow(q \cdot x) = q \cdot (\uparrow x)$, where $\uparrow$ denotes the canonical inclusion map from $s$ to $K$.

SubfieldClass.coe_qsmul theorem

(s : S) (q : ℚ) (x : s) : ↑(q • x) = q • (x : K)

Full source

@[simp, norm_cast] lemma coe_qsmul (s : S) (q : ℚ) (x : s) : ↑(q • x) = q • (x : K) := rfl

Compatibility of Scalar Multiplication with Rationals in Subfields

Informal description

For any subfield $s$ of a division ring $K$, any rational number $q \in \mathbb{Q}$, and any element $x \in s$, the canonical inclusion map $\uparrow$ satisfies $\uparrow(q \cdot x) = q \cdot (\uparrow x)$, where the scalar multiplication on the left is in $s$ and on the right is in $K$.

SubfieldClass.toDivisionRing instance

(s : S) : DivisionRing s

Full source

/-- A subfield inherits a division ring structure -/
instance (priority := 75) toDivisionRing (s : S) : DivisionRing s := fast_instance%
  Subtype.coe_injective.divisionRing ((↑) : s → K)
    rfl rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl)
    (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl) (coe_nnqsmul _) (coe_qsmul _) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl)

Subfields Inherit Division Ring Structure

Informal description

For any subfield $s$ of a division ring $K$, the subset $s$ inherits a division ring structure from $K$. This means that $s$ is equipped with addition, multiplication, additive inverses, and multiplicative inverses for nonzero elements, satisfying all the axioms of a division ring.

SubfieldClass.toField instance

{K} [Field K] [SetLike S K] [SubfieldClass S K] (s : S) : Field s

Full source

/-- A subfield of a field inherits a field structure -/
instance (priority := 75) toField {K} [Field K] [SetLike S K] [SubfieldClass S K] (s : S) :
    Field s := fast_instance%
  Subtype.coe_injective.field ((↑) : s → K)
    rfl rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl)
    (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (coe_nnqsmul _) (coe_qsmul _) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl)
    (fun _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl)

Subfields Inherit Field Structure

Informal description

For any field $K$ and any subfield $s$ of $K$ (in the sense of `SubfieldClass`), $s$ inherits a field structure from $K$.

Subfield structure

(K : Type u) [DivisionRing K] extends Subring K

Full source

/-- `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. -/
@[stacks 09FD "second part"]
structure Subfield (K : Type u) [DivisionRing K] extends Subring K where
  /-- A subfield is closed under multiplicative inverses. -/
  inv_mem' : ∀ x ∈ carrier, x⁻¹ ∈ carrier

Subfield of a division ring

Informal description

A subfield of a division ring $ K $ is a subset of $ K $ that is closed under addition, multiplication, contains the additive and multiplicative identities, and is closed under taking additive inverses and multiplicative inverses of non-zero elements. Formally, a subfield $ S $ of $ K $ is a structure that extends the notion of a subring, ensuring that $ S $ is also closed under the division operation (i.e., for any non-zero $ x \in S $, the inverse $ x^{-1} $ is also in $ S $).

Subfield.toAddSubgroup definition

(s : Subfield K) : AddSubgroup K

Full source

/-- The underlying `AddSubgroup` of a subfield. -/
def toAddSubgroup (s : Subfield K) : AddSubgroup K :=
  { s.toSubring.toAddSubgroup with }

Additive subgroup of a subfield

Informal description

Given a subfield $ s $ of a division ring $ K $, the function returns the underlying additive subgroup of $ K $ corresponding to $ s $. This additive subgroup consists of all elements of $ s $ considered under the addition operation of $ K $.

Subfield.instSetLike instance

: SetLike (Subfield K) K

Full source

instance : SetLike (Subfield K) K where
  coe s := s.carrier
  coe_injective' p q h := by cases p; cases q; congr; exact SetLike.ext' h

Set-like Structure for Subfields of a Division Ring

Informal description

The type of subfields of a division ring $K$ has a set-like structure, where each subfield can be viewed as a subset of $K$ with an injective coercion map.

Subfield.instSubfieldClass instance

: SubfieldClass (Subfield K) K

Full source

instance : SubfieldClass (Subfield K) K where
  add_mem {s} := s.add_mem'
  zero_mem s := s.zero_mem'
  neg_mem {s} := s.neg_mem'
  mul_mem {s} := s.mul_mem'
  one_mem s := s.one_mem'
  inv_mem {s} := s.inv_mem' _

Subfields as SubfieldClass Instances

Informal description

The type of subfields of a division ring $K$ forms a `SubfieldClass`, meaning it inherits the properties of both `SubringClass` (closure under addition, multiplication, and additive inverses) and `InvMemClass` (closure under multiplicative inverses for nonzero elements).

Subfield.mem_carrier theorem

{s : Subfield K} {x : K} : x ∈ s.carrier ↔ x ∈ s

Full source

theorem mem_carrier {s : Subfield K} {x : K} : x ∈ s.carrierx ∈ s.carrier ↔ x ∈ s :=
  Iff.rfl

Membership in Subfield Carrier Set

Informal description

For any subfield $s$ of a division ring $K$ and any element $x \in K$, the element $x$ belongs to the underlying set of $s$ if and only if $x$ is a member of $s$ as a subfield.

Subfield.mem_mk theorem

{S : Subring K} {x : K} (h) : x ∈ (⟨S, h⟩ : Subfield K) ↔ x ∈ S

Full source

@[simp]
theorem mem_mk {S : Subring K} {x : K} (h) : x ∈ (⟨S, h⟩ : Subfield K)x ∈ (⟨S, h⟩ : Subfield K) ↔ x ∈ S :=
  Iff.rfl

Membership in Generated Subfield of a Subring

Informal description

Let $K$ be a division ring, $S$ be a subring of $K$, and $x \in K$. Then $x$ belongs to the subfield generated by $S$ (with closure condition $h$) if and only if $x$ belongs to $S$.

Subfield.coe_set_mk theorem

(S : Subring K) (h) : ((⟨S, h⟩ : Subfield K) : Set K) = S

Full source

@[simp]
theorem coe_set_mk (S : Subring K) (h) : ((⟨S, h⟩ : Subfield K) : Set K) = S :=
  rfl

Subfield Construction Preserves Underlying Set

Informal description

Given a subring $S$ of a division ring $K$ and a proof $h$ that $S$ is closed under multiplicative inverses, the underlying set of the subfield $\langle S, h \rangle$ is equal to $S$ as a set.

Subfield.mk_le_mk theorem

{S S' : Subring K} (h h') : (⟨S, h⟩ : Subfield K) ≤ (⟨S', h'⟩ : Subfield K) ↔ S ≤ S'

Full source

@[simp]
theorem mk_le_mk {S S' : Subring K} (h h') : (⟨S, h⟩ : Subfield K) ≤ (⟨S', h'⟩ : Subfield K) ↔
    S ≤ S' :=
  Iff.rfl

Subfield Inclusion Criterion via Subring Inclusion

Informal description

Let $K$ be a division ring, and let $S$ and $S'$ be subrings of $K$ with closure conditions $h$ and $h'$ under multiplicative inverses, respectively. Then the subfield generated by $S$ is contained in the subfield generated by $S'$ if and only if $S$ is contained in $S'$ as subrings.

Subfield.ext theorem

{S T : Subfield K} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T

Full source

/-- Two subfields are equal if they have the same elements. -/
@[ext]
theorem ext {S T : Subfield K} (h : ∀ x, x ∈ Sx ∈ S ↔ x ∈ T) : S = T :=
  SetLike.ext h

Extensionality of Subfields: $S = T \iff \forall x, x \in S \leftrightarrow x \in T$

Informal description

Two subfields $S$ and $T$ of a division ring $K$ are equal if and only if they contain the same elements, i.e., for every $x \in K$, $x \in S$ if and only if $x \in T$.

Subfield.copy definition

(S : Subfield K) (s : Set K) (hs : s = ↑S) : Subfield K

Full source

/-- Copy of a subfield with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (S : Subfield K) (s : Set K) (hs : s = ↑S) : Subfield K :=
  { S.toSubring.copy s hs with
    carrier := s
    inv_mem' := hs.symm ▸ S.inv_mem' }

Copy of a subfield with a specified carrier set

Informal description

Given a subfield $ S $ of a division ring $ K $ and a subset $ s $ of $ K $ that is equal to the underlying set of $ S $, the function `Subfield.copy` constructs a new subfield with carrier $ s $. This is useful for fixing definitional equalities when working with subfields.

Subfield.coe_copy theorem

(S : Subfield K) (s : Set K) (hs : s = ↑S) : (S.copy s hs : Set K) = s

Full source

@[simp]
theorem coe_copy (S : Subfield K) (s : Set K) (hs : s = ↑S) : (S.copy s hs : Set K) = s :=
  rfl

Underlying Set Equality for Copied Subfield: $(S.\text{copy}\ s\ hs) = s$

Informal description

Given a subfield $S$ of a division ring $K$ and a subset $s$ of $K$ such that $s$ equals the underlying set of $S$, the underlying set of the copied subfield $S.\text{copy}\ s\ hs$ is equal to $s$.

Subfield.copy_eq theorem

(S : Subfield K) (s : Set K) (hs : s = ↑S) : S.copy s hs = S

Full source

theorem copy_eq (S : Subfield K) (s : Set K) (hs : s = ↑S) : S.copy s hs = S :=
  SetLike.coe_injective hs

Equality of Subfield Copy with Original Subfield

Informal description

For any subfield $S$ of a division ring $K$ and any subset $s$ of $K$ such that $s$ equals the underlying set of $S$, the subfield $S.\text{copy}(s, hs)$ is equal to $S$.

Subfield.coe_toSubring theorem

(s : Subfield K) : (s.toSubring : Set K) = s

Full source

@[simp]
theorem coe_toSubring (s : Subfield K) : (s.toSubring : Set K) = s :=
  rfl

Equality of Subring and Subfield Carrier Sets

Informal description

For any subfield $s$ of a division ring $K$, the underlying set of $s$ as a subring is equal to the underlying set of $s$ as a subfield.

Subfield.mem_toSubring theorem

(s : Subfield K) (x : K) : x ∈ s.toSubring ↔ x ∈ s

Full source

@[simp]
theorem mem_toSubring (s : Subfield K) (x : K) : x ∈ s.toSubringx ∈ s.toSubring ↔ x ∈ s :=
  Iff.rfl

Equivalence of Membership in Subfield and its Underlying Subring

Informal description

For any subfield $s$ of a division ring $K$ and any element $x \in K$, $x$ belongs to the underlying subring of $s$ if and only if $x$ belongs to $s$.

Subring.toSubfield definition

(s : Subring K) (hinv : ∀ x ∈ s, x⁻¹ ∈ s) : Subfield K

Full source

/-- A `Subring` containing inverses is a `Subfield`. -/
def Subring.toSubfield (s : Subring K) (hinv : ∀ x ∈ s, x⁻¹ ∈ s) : Subfield K :=
  { s with inv_mem' := hinv }

Subring with inverses is a subfield

Informal description

Given a subring $ s $ of a division ring $ K $ such that for every element $ x \in s $, the multiplicative inverse $ x^{-1} $ is also in $ s $, the structure $ s $ can be extended to a subfield of $ K $.

Subfield.one_mem theorem

: (1 : K) ∈ s

Full source

/-- A subfield contains the field's 1. -/
protected theorem one_mem : (1 : K) ∈ s :=
  one_mem s

Subfield Contains One

Informal description

For any subfield $s$ of a division ring $K$, the multiplicative identity $1$ is an element of $s$.

Subfield.zero_mem theorem

: (0 : K) ∈ s

Full source

/-- A subfield contains the field's 0. -/
protected theorem zero_mem : (0 : K) ∈ s :=
  zero_mem s

Subfield Contains Zero

Informal description

For any subfield $s$ of a division ring $K$, the additive identity $0$ is an element of $s$.

Subfield.mul_mem theorem

{x y : K} : x ∈ s → y ∈ s → x * y ∈ s

Full source

/-- A subfield is closed under multiplication. -/
protected theorem mul_mem {x y : K} : x ∈ s → y ∈ s → x * y ∈ s :=
  mul_mem

Closure under multiplication in a subfield

Informal description

For any subfield $s$ of a division ring $K$ and any elements $x, y \in K$, if $x$ and $y$ belong to $s$, then their product $x * y$ also belongs to $s$.

Subfield.add_mem theorem

{x y : K} : x ∈ s → y ∈ s → x + y ∈ s

Full source

/-- A subfield is closed under addition. -/
protected theorem add_mem {x y : K} : x ∈ s → y ∈ s → x + y ∈ s :=
  add_mem

Closure of Subfield under Addition

Informal description

Let $K$ be a division ring and $s$ be a subfield of $K$. For any elements $x, y \in K$, if $x \in s$ and $y \in s$, then their sum $x + y$ is also in $s$.

Subfield.neg_mem theorem

{x : K} : x ∈ s → -x ∈ s

Full source

/-- A subfield is closed under negation. -/
protected theorem neg_mem {x : K} : x ∈ s → -x ∈ s :=
  neg_mem

Closure under Negation in Subfields

Informal description

For any subfield $s$ of a division ring $K$ and any element $x \in s$, the additive inverse $-x$ is also in $s$.

Subfield.sub_mem theorem

{x y : K} : x ∈ s → y ∈ s → x - y ∈ s

Full source

/-- A subfield is closed under subtraction. -/
protected theorem sub_mem {x y : K} : x ∈ s → y ∈ s → x - y ∈ s :=
  sub_mem

Closure under subtraction in a subfield

Informal description

For any subfield $s$ of a division ring $K$ and any elements $x, y \in K$, if $x$ and $y$ belong to $s$, then their difference $x - y$ also belongs to $s$.

Subfield.inv_mem theorem

{x : K} : x ∈ s → x⁻¹ ∈ s

Full source

/-- A subfield is closed under inverses. -/
protected theorem inv_mem {x : K} : x ∈ s → x⁻¹x⁻¹ ∈ s :=
  inv_mem

Subfields are closed under inverses

Informal description

For any subfield $s$ of a division ring $K$ and any element $x \in s$, the multiplicative inverse $x^{-1}$ is also in $s$.

Subfield.div_mem theorem

{x y : K} : x ∈ s → y ∈ s → x / y ∈ s

Full source

/-- A subfield is closed under division. -/
protected theorem div_mem {x y : K} : x ∈ s → y ∈ s → x / y ∈ s :=
  div_mem

Closure of Subfield under Division

Informal description

Let $K$ be a division ring and $s$ a subfield of $K$. For any elements $x, y \in K$, if $x \in s$ and $y \in s$, then their quotient $x / y$ is also in $s$.

Subfield.pow_mem theorem

{x : K} (hx : x ∈ s) (n : ℕ) : x ^ n ∈ s

Full source

protected theorem pow_mem {x : K} (hx : x ∈ s) (n : ℕ) : x ^ n ∈ s :=
  pow_mem hx n

Closure under Powers in Subfields

Informal description

Let $K$ be a division ring and $s$ a subfield of $K$. For any element $x \in s$ and any natural number $n$, the power $x^n$ belongs to $s$.

Subfield.zsmul_mem theorem

{x : K} (hx : x ∈ s) (n : ℤ) : n • x ∈ s

Full source

protected theorem zsmul_mem {x : K} (hx : x ∈ s) (n : ℤ) : n • x ∈ s :=
  zsmul_mem hx n

Closure under Integer Scalar Multiplication in Subfields

Informal description

For any element $x$ in a subfield $s$ of a division ring $K$ and any integer $n$, the integer scalar multiple $n \cdot x$ belongs to $s$.

Subfield.intCast_mem theorem

(n : ℤ) : (n : K) ∈ s

Full source

protected theorem intCast_mem (n : ℤ) : (n : K) ∈ s := intCast_mem s n

Integer Elements Belong to Subfield

Informal description

For any integer $n$, the canonical image of $n$ in the division ring $K$ belongs to the subfield $s$.

Subfield.zpow_mem theorem

{x : K} (hx : x ∈ s) (n : ℤ) : x ^ n ∈ s

Full source

theorem zpow_mem {x : K} (hx : x ∈ s) (n : ℤ) : x ^ n ∈ s := by
  cases n
  · simpa using s.pow_mem hx _
  · simpa [pow_succ'] using s.inv_mem (s.mul_mem hx (s.pow_mem hx _))

Closure under Integer Powers in Subfields

Informal description

For any element $x$ in a subfield $s$ of a division ring $K$ and any integer $n$, the power $x^n$ belongs to $s$.

Subfield.instRingSubtypeMem instance

: Ring s

Full source

instance : Ring s :=
  s.toSubring.toRing

Ring Structure on Subfields

Informal description

For any subfield $s$ of a division ring $K$, the subset $s$ inherits a ring structure from $K$.

Subfield.instDivSubtypeMem instance

: Div s

Full source

instance : Div s :=
  ⟨fun x y => ⟨x / y, s.div_mem x.2 y.2⟩⟩

Subfields are Closed under Division

Informal description

For any subfield $s$ of a division ring $K$, the subset $s$ is closed under the division operation.

Subfield.instInvSubtypeMem instance

: Inv s

Full source

instance : Inv s :=
  ⟨fun x => ⟨x⁻¹, s.inv_mem x.2⟩⟩

Subfields are Closed under Inversion

Informal description

For any subfield $s$ of a division ring $K$, the subset $s$ is closed under the multiplicative inverse operation.

Subfield.instPowSubtypeMemInt instance

: Pow s ℤ

Full source

instance : Pow s ℤ :=
  ⟨fun x z => ⟨x ^ z, s.zpow_mem x.2 z⟩⟩

Integer Powers in Subfields

Informal description

For any subfield $s$ of a division ring $K$, the subset $s$ is equipped with a canonical integer power operation $s \times \mathbb{Z} \to s$.

Subfield.toDivisionRing instance

(s : Subfield K) : DivisionRing s

Full source

instance toDivisionRing (s : Subfield K) : DivisionRing s := fast_instance%
  Subtype.coe_injective.divisionRing ((↑) : s → K) rfl rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl)
    (fun _ ↦ rfl) fun _ ↦ rfl

Subfields Inherit Division Ring Structure

Informal description

For any subfield $s$ of a division ring $K$, the subset $s$ inherits a division ring structure from $K$.

Subfield.toField instance

{K} [Field K] (s : Subfield K) : Field s

Full source

/-- A subfield inherits a field structure -/
instance toField {K} [Field K] (s : Subfield K) : Field s := fast_instance%
  Subtype.coe_injective.field ((↑) : s → K) rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl)
    (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ ↦ rfl) (fun _ => rfl)
    (fun _ => rfl) (fun _ ↦ rfl) fun _ => rfl

Subfields Inherit Field Structure

Informal description

For any field $K$ and any subfield $s$ of $K$, the subset $s$ inherits a field structure from $K$.

Subfield.coe_add theorem

(x y : s) : (↑(x + y) : K) = ↑x + ↑y

Full source

@[simp, norm_cast]
theorem coe_add (x y : s) : (↑(x + y) : K) = ↑x + ↑y :=
  rfl

Addition in Subfield Preserves Canonical Inclusion

Informal description

For any elements $x$ and $y$ in a subfield $s$ of a division ring $K$, the canonical inclusion map $\uparrow$ satisfies $\uparrow(x + y) = \uparrow x + \uparrow y$ in $K$.

Subfield.coe_sub theorem

(x y : s) : (↑(x - y) : K) = ↑x - ↑y

Full source

@[simp, norm_cast]
theorem coe_sub (x y : s) : (↑(x - y) : K) = ↑x - ↑y :=
  rfl

Subtraction in Subfield Preserves Canonical Inclusion

Informal description

For any elements $x$ and $y$ in a subfield $s$ of a division ring $K$, the canonical inclusion map $\uparrow$ satisfies $\uparrow(x - y) = \uparrow x - \uparrow y$ in $K$.

Subfield.coe_neg theorem

(x : s) : (↑(-x) : K) = -↑x

Full source

@[simp, norm_cast]
theorem coe_neg (x : s) : (↑(-x) : K) = -↑x :=
  rfl

Negation Preserved by Subfield Inclusion

Informal description

For any element $x$ in a subfield $s$ of a division ring $K$, the canonical inclusion map $\uparrow$ satisfies $\uparrow(-x) = -\uparrow x$ in $K$.

Subfield.coe_mul theorem

(x y : s) : (↑(x * y) : K) = ↑x * ↑y

Full source

@[simp, norm_cast]
theorem coe_mul (x y : s) : (↑(x * y) : K) = ↑x * ↑y :=
  rfl

Coercion Preserves Multiplication in Subfields

Informal description

For any elements $x$ and $y$ in a subfield $s$ of a division ring $K$, the coercion of their product $x \cdot y$ in $K$ is equal to the product of their coercions, i.e., $\overline{x \cdot y} = \overline{x} \cdot \overline{y}$.

Subfield.coe_div theorem

(x y : s) : (↑(x / y) : K) = ↑x / ↑y

Full source

@[simp, norm_cast]
theorem coe_div (x y : s) : (↑(x / y) : K) = ↑x / ↑y :=
  rfl

Division in Subfield Preserved by Inclusion

Informal description

For any elements $x$ and $y$ in a subfield $s$ of a division ring $K$, the canonical inclusion map $\uparrow$ satisfies $\uparrow(x / y) = \uparrow x / \uparrow y$ in $K$.

Subfield.coe_inv theorem

(x : s) : (↑x⁻¹ : K) = (↑x)⁻¹

Full source

@[simp, norm_cast]
theorem coe_inv (x : s) : (↑x⁻¹ : K) = (↑x)⁻¹ :=
  rfl

Inclusion Preserves Inverses in Subfields

Informal description

For any element $x$ in a subfield $s$ of a division ring $K$, the canonical inclusion of the inverse $x^{-1}$ in $K$ is equal to the inverse of the canonical inclusion of $x$ in $K$, i.e., $\overline{x^{-1}} = (\overline{x})^{-1}$.

Subfield.coe_zero theorem

: ((0 : s) : K) = 0

Full source

@[simp, norm_cast]
theorem coe_zero : ((0 : s) : K) = 0 :=
  rfl

Inclusion of Zero in Subfield Preserves Zero

Informal description

For any subfield $s$ of a division ring $K$, the canonical inclusion of the zero element of $s$ into $K$ is equal to the zero element of $K$, i.e., $\overline{0_s} = 0_K$.

Subfield.coe_one theorem

: ((1 : s) : K) = 1

Full source

@[simp, norm_cast]
theorem coe_one : ((1 : s) : K) = 1 :=
  rfl

Inclusion Preserves Identity in Subfields

Informal description

For any subfield $s$ of a division ring $K$, the canonical inclusion of the multiplicative identity $1$ in $s$ into $K$ is equal to the multiplicative identity $1$ in $K$, i.e., $\overline{1_s} = 1_K$.

Subfield.subtype definition

(s : Subfield K) : s →+* K

Full source

/-- The embedding from a subfield of the field `K` to `K`. -/
def subtype (s : Subfield K) : s →+* K :=
  { s.toSubmonoid.subtype, s.toAddSubgroup.subtype with toFun := (↑) }

Inclusion homomorphism of a subfield

Informal description

The canonical ring homomorphism from a subfield $ s $ of a division ring $ K $ to $ K $, which maps each element of $ s $ to itself in $ K $. This homomorphism preserves both the additive and multiplicative structures of $ s $.

Subfield.subtype_apply theorem

{s : Subfield K} (x : s) : s.subtype x = x

Full source

@[simp]
lemma subtype_apply {s : Subfield K} (x : s) :
    s.subtype x = x := rfl

Inclusion Homomorphism Acts as Identity on Subfield Elements

Informal description

For any subfield $s$ of a division ring $K$ and any element $x \in s$, the inclusion homomorphism $\text{subtype}(s)$ maps $x$ to itself in $K$, i.e., $\text{subtype}(s)(x) = x$.

Subfield.subtype_injective theorem

(s : Subfield K) : Function.Injective s.subtype

Full source

lemma subtype_injective (s : Subfield K) :
    Function.Injective s.subtype :=
  Subtype.coe_injective

Injectivity of Subfield Inclusion Homomorphism

Informal description

For any subfield $s$ of a division ring $K$, the inclusion homomorphism $s \hookrightarrow K$ is injective. That is, if two elements of $s$ are equal in $K$, then they are equal in $s$.

Subfield.coe_subtype theorem

: ⇑(s.subtype) = ((↑) : s → K)

Full source

@[simp]
theorem coe_subtype : ⇑(s.subtype) = ((↑) : s → K) :=
  rfl

Inclusion Homomorphism Equals Coercion for Subfields

Informal description

The inclusion homomorphism $\text{subtype}$ from a subfield $s$ of a division ring $K$ to $K$ coincides with the canonical coercion map from $s$ to $K$. That is, for any $x \in s$, we have $\text{subtype}(x) = x$.

Subfield.toSubring_subtype_eq_subtype theorem

(S : Subfield K) : S.toSubring.subtype = S.subtype

Full source

theorem toSubring_subtype_eq_subtype (S : Subfield K) :
    S.toSubring.subtype = S.subtype :=
  rfl

Subfield and Subring Inclusion Homomorphism Coincidence

Informal description

For any subfield $S$ of a division ring $K$, the inclusion homomorphism from the underlying subring of $S$ to $K$ coincides with the inclusion homomorphism from $S$ to $K$.

Subfield.mem_toSubmonoid theorem

{s : Subfield K} {x : K} : x ∈ s.toSubmonoid ↔ x ∈ s

Full source

theorem mem_toSubmonoid {s : Subfield K} {x : K} : x ∈ s.toSubmonoidx ∈ s.toSubmonoid ↔ x ∈ s :=
  Iff.rfl

Membership Equivalence between Subfield and Associated Submonoid

Informal description

For any subfield $s$ of a division ring $K$ and any element $x \in K$, $x$ belongs to the submonoid associated with $s$ if and only if $x$ belongs to $s$.

Subfield.coe_toSubmonoid theorem

: (s.toSubmonoid : Set K) = s

Full source

@[simp]
theorem coe_toSubmonoid : (s.toSubmonoid : Set K) = s :=
  rfl

Subfield to Submonoid Coercion Equality

Informal description

For any subfield $s$ of a division ring $K$, the underlying set of the submonoid associated with $s$ is equal to $s$ itself, i.e., $(s.\text{toSubmonoid} : \text{Set } K) = s$.

Subfield.mem_toAddSubgroup theorem

{s : Subfield K} {x : K} : x ∈ s.toAddSubgroup ↔ x ∈ s

Full source

@[simp]
theorem mem_toAddSubgroup {s : Subfield K} {x : K} : x ∈ s.toAddSubgroupx ∈ s.toAddSubgroup ↔ x ∈ s :=
  Iff.rfl

Membership Equivalence between Subfield and Associated Additive Subgroup

Informal description

For any subfield $s$ of a division ring $K$ and any element $x \in K$, $x$ belongs to the additive subgroup associated with $s$ if and only if $x$ belongs to $s$.

Subfield.coe_toAddSubgroup theorem

: (s.toAddSubgroup : Set K) = s

Full source

@[simp]
theorem coe_toAddSubgroup : (s.toAddSubgroup : Set K) = s :=
  rfl

Equality of Subfield and its Additive Subgroup's Underlying Set

Informal description

For any subfield $s$ of a division ring $K$, the underlying set of the additive subgroup associated with $s$ is equal to $s$ itself, i.e., $(s.\text{toAddSubgroup} : \text{Set } K) = s$.

Mathlib.Algebra.Field.Subfield.Defs

Main definitions

Implementation notes

Tags