Mathlib.Data.Rat.Cast.CharZero

Rat.cast_injective theorem

: Injective ((↑) : ℚ → α)

Full source

@[stacks 09FR "Characteristic zero case."]
lemma cast_injective : Injective ((↑) : ℚ → α)
  | ⟨n₁, d₁, d₁0, c₁⟩, ⟨n₂, d₂, d₂0, c₂⟩, h => by
    have d₁a : (d₁ : α) ≠ 0 := Nat.cast_ne_zero.2 d₁0
    have d₂a : (d₂ : α) ≠ 0 := Nat.cast_ne_zero.2 d₂0
    rw [mk'_eq_divInt, mk'_eq_divInt] at h ⊢
    rw [cast_divInt_of_ne_zero, cast_divInt_of_ne_zero] at h <;> simp [d₁0, d₂0] at h ⊢
    rwa [eq_div_iff_mul_eq d₂a, division_def, mul_assoc, (d₁.cast_commute (d₂ : α)).inv_left₀.eq, ←
      mul_assoc, ← division_def, eq_comm, eq_div_iff_mul_eq d₁a, eq_comm, ← Int.cast_natCast d₁, ←
      Int.cast_mul, ← Int.cast_natCast d₂, ← Int.cast_mul, Int.cast_inj, ← mkRat_eq_iff d₁0 d₂0]
      at h

Injectivity of Rational Number Cast into Characteristic Zero Fields

Informal description

The canonical map from the rational numbers $\mathbb{Q}$ to a characteristic zero field (or division ring) $\alpha$ is injective.

Rat.cast_inj theorem

: (p : α) = q ↔ p = q

Full source

@[simp, norm_cast] lemma cast_inj : (p : α) = q ↔ p = q := cast_injective.eq_iff

Injectivity of Rational Number Cast: $(p : \alpha) = (q : \alpha) \leftrightarrow p = q$

Informal description

For any rational numbers $p$ and $q$ and any characteristic zero field (or division ring) $\alpha$, the canonical map $\mathbb{Q} \to \alpha$ satisfies $(p : \alpha) = (q : \alpha)$ if and only if $p = q$.

Rat.cast_eq_zero theorem

: (p : α) = 0 ↔ p = 0

Full source

@[simp, norm_cast] lemma cast_eq_zero : (p : α) = 0 ↔ p = 0 := cast_injective.eq_iff' cast_zero

Rational Cast to Zero in Characteristic Zero Fields: $(p : \alpha) = 0 \leftrightarrow p = 0$

Informal description

For any rational number $p$ and any characteristic zero field (or division ring) $\alpha$, the canonical map $\mathbb{Q} \to \alpha$ satisfies $(p : \alpha) = 0$ if and only if $p = 0$.

Rat.cast_ne_zero theorem

: (p : α) ≠ 0 ↔ p ≠ 0

Full source

lemma cast_ne_zero : (p : α) ≠ 0(p : α) ≠ 0 ↔ p ≠ 0 := cast_eq_zero.ne

Nonzero Preservation in Rational Number Cast: $(p : \alpha) \neq 0 \leftrightarrow p \neq 0$

Informal description

For any rational number $p$ and any characteristic zero field (or division ring) $\alpha$, the canonical map $\mathbb{Q} \to \alpha$ satisfies $(p : \alpha) \neq 0$ if and only if $p \neq 0$.

Rat.cast_add theorem

(p q : ℚ) : ↑(p + q) = (p + q : α)

Full source

@[simp, norm_cast] lemma cast_add (p q : ℚ) : ↑(p + q) = (p + q : α) :=
  cast_add_of_ne_zero (Nat.cast_ne_zero.2 p.pos.ne') (Nat.cast_ne_zero.2 q.pos.ne')

Addition Preservation in Rational Number Cast to Characteristic Zero Field

Informal description

For any rational numbers $p$ and $q$, the canonical map from $\mathbb{Q}$ to a characteristic zero field (or division ring) $\alpha$ preserves addition, i.e., $(p + q) = p + q$ in $\alpha$.

Rat.cast_sub theorem

(p q : ℚ) : ↑(p - q) = (p - q : α)

Full source

@[simp, norm_cast] lemma cast_sub (p q : ℚ) : ↑(p - q) = (p - q : α) :=
  cast_sub_of_ne_zero (Nat.cast_ne_zero.2 p.pos.ne') (Nat.cast_ne_zero.2 q.pos.ne')

Subtraction Preservation under Rational Number Casting in Characteristic Zero Fields

Informal description

For any rational numbers $p$ and $q$, the canonical map from the rationals to a characteristic zero field (or division ring) $\alpha$ preserves subtraction, i.e., $\overline{p - q} = \overline{p} - \overline{q}$ where $\overline{\cdot}$ denotes the canonical map.

Rat.cast_mul theorem

(p q : ℚ) : ↑(p * q) = (p * q : α)

Full source

@[simp, norm_cast] lemma cast_mul (p q : ℚ) : ↑(p * q) = (p * q : α) :=
  cast_mul_of_ne_zero (Nat.cast_ne_zero.2 p.pos.ne') (Nat.cast_ne_zero.2 q.pos.ne')

Multiplication Preservation under Rational Number Casting

Informal description

For any rational numbers $p$ and $q$, the canonical map from the rationals to a characteristic zero field (or division ring) $\alpha$ preserves multiplication, i.e., $\uparrow(p \cdot q) = \uparrow p \cdot \uparrow q$ in $\alpha$.

Rat.castHom definition

: ℚ →+* α

Full source

/-- Coercion `ℚ → α` as a `RingHom`. -/
def castHom : ℚℚ →+* α where
  toFun := (↑)
  map_one' := cast_one
  map_mul' := cast_mul
  map_zero' := cast_zero
  map_add' := cast_add

Canonical ring homomorphism from rationals to a characteristic zero field

Informal description

The ring homomorphism that maps a rational number $q$ to its canonical image in a characteristic zero field (or division ring) $\alpha$. This map preserves addition, multiplication, zero, and one, i.e., it satisfies: - $\text{castHom}(1) = 1$ - $\text{castHom}(p + q) = \text{castHom}(p) + \text{castHom}(q)$ - $\text{castHom}(p \cdot q) = \text{castHom}(p) \cdot \text{castHom}(q)$ - $\text{castHom}(0) = 0$

Rat.coe_castHom theorem

: ⇑(castHom α) = ((↑) : ℚ → α)

Full source

@[simp] lemma coe_castHom : ⇑(castHom α) = ((↑) : ℚ → α) := rfl

Canonical Homomorphism Coincides with Rational Embedding in Characteristic Zero Fields

Informal description

The canonical ring homomorphism $\text{castHom}_\alpha$ from the rational numbers $\mathbb{Q}$ to a characteristic zero field (or division ring) $\alpha$ coincides with the canonical embedding $\uparrow : \mathbb{Q} \to \alpha$, i.e., $\text{castHom}_\alpha(q) = \uparrow q$ for all $q \in \mathbb{Q}$.

Rat.cast_inv theorem

(p : ℚ) : ↑(p⁻¹) = (p⁻¹ : α)

Full source

@[simp, norm_cast] lemma cast_inv (p : ℚ) : ↑(p⁻¹) = (p⁻¹ : α) := map_inv₀ (castHom α) _

Preservation of Inversion under Rational Number Casting

Informal description

For any rational number $p$, the canonical map from $\mathbb{Q}$ to a characteristic zero field (or division ring) $\alpha$ preserves inversion, i.e., $\uparrow(p^{-1}) = (\uparrow p)^{-1}$ in $\alpha$.

Rat.cast_div theorem

(p q : ℚ) : ↑(p / q) = (p / q : α)

Full source

@[simp, norm_cast] lemma cast_div (p q : ℚ) : ↑(p / q) = (p / q : α) := map_div₀ (castHom α) ..

Preservation of Division under Rational Number Casting

Informal description

For any rational numbers $p$ and $q$, the canonical map from $\mathbb{Q}$ to a characteristic zero field (or division ring) $\alpha$ preserves division, i.e., $\uparrow(p / q) = (\uparrow p) / (\uparrow q)$ in $\alpha$.

Rat.cast_zpow theorem

(p : ℚ) (n : ℤ) : ↑(p ^ n) = (p ^ n : α)

Full source

@[simp, norm_cast]
lemma cast_zpow (p : ℚ) (n : ℤ) : ↑(p ^ n) = (p ^ n : α) := map_zpow₀ (castHom α) ..

Preservation of Integer Powers under Rational Number Casting

Informal description

For any rational number $p$ and integer $n$, the canonical map from rational numbers to a characteristic zero field (or division ring) $\alpha$ preserves integer powers, i.e., $\uparrow(p^n) = (\uparrow p)^n$ in $\alpha$.

Rat.cast_mk theorem

(a b : ℤ) : (a /. b : α) = a / b

Full source

@[norm_cast]
theorem cast_mk (a b : ℤ) : (a /. b : α) = a / b := by
  simp only [divInt_eq_div, cast_div, cast_intCast]

Rational Construction Preserves Division under Casting: $\left(\frac{a}{b} : \alpha\right) = \frac{a}{b}$

Informal description

For any integers $a$ and $b$, the canonical map from the rational number $\frac{a}{b}$ (constructed as `a /. b`) to a characteristic zero field (or division ring) $\alpha$ is equal to the division of the images of $a$ and $b$ in $\alpha$, i.e., $\left(\frac{a}{b} : \alpha\right) = \frac{a}{b}$.

NNRat.cast_injective theorem

: Injective ((↑) : ℚ≥0 → α)

Full source

lemma cast_injective : Injective ((↑) : ℚ≥0 → α) := by
  rintro p q hpq
  rw [NNRat.cast_def, NNRat.cast_def, Commute.div_eq_div_iff] at hpq
  on_goal 1 => rw [← p.num_div_den, ← q.num_div_den, div_eq_div_iff]
  · norm_cast at hpq ⊢
  any_goals norm_cast
  any_goals apply den_ne_zero
  exact Nat.cast_commute ..

Injectivity of the Canonical Map from Nonnegative Rationals to Characteristic Zero Fields

Informal description

The canonical map from nonnegative rational numbers to a characteristic zero field (or division ring) $\alpha$ is injective. That is, for any $p, q \in \mathbb{Q}_{\geq 0}$, if $p = q$ in $\alpha$, then $p = q$ in $\mathbb{Q}_{\geq 0}$.

NNRat.cast_inj theorem

: (p : α) = q ↔ p = q

Full source

@[simp, norm_cast] lemma cast_inj : (p : α) = q ↔ p = q := cast_injective.eq_iff

Injectivity of Nonnegative Rationals Cast into Characteristic Zero Fields: $(p : \alpha) = (q : \alpha) \leftrightarrow p = q$

Informal description

For any nonnegative rational numbers $p$ and $q$, and for any characteristic zero field (or division ring) $\alpha$, the canonical map from $\mathbb{Q}_{\geq 0}$ to $\alpha$ satisfies $(p : \alpha) = (q : \alpha)$ if and only if $p = q$ in $\mathbb{Q}_{\geq 0}$.

NNRat.cast_eq_zero theorem

: (q : α) = 0 ↔ q = 0

Full source

@[simp, norm_cast] lemma cast_eq_zero : (q : α) = 0 ↔ q = 0 := by rw [← cast_zero, cast_inj]

Zero Preservation under Canonical Map from Nonnegative Rationals to Characteristic Zero Field: $(q : \alpha) = 0 \leftrightarrow q = 0$

Informal description

For any nonnegative rational number $q$ and any characteristic zero field (or division ring) $\alpha$, the canonical map from $\mathbb{Q}_{\geq 0}$ to $\alpha$ satisfies $(q : \alpha) = 0$ if and only if $q = 0$ in $\mathbb{Q}_{\geq 0}$.

NNRat.cast_ne_zero theorem

: (q : α) ≠ 0 ↔ q ≠ 0

Full source

lemma cast_ne_zero : (q : α) ≠ 0(q : α) ≠ 0 ↔ q ≠ 0 := cast_eq_zero.not

Nonzero Preservation under Canonical Map from Nonnegative Rationals to Characteristic Zero Field: $(q : \alpha) \neq 0 \leftrightarrow q \neq 0$

Informal description

For any nonnegative rational number $q$ and any characteristic zero field (or division ring) $\alpha$, the canonical map from $\mathbb{Q}_{\geq 0}$ to $\alpha$ satisfies $(q : \alpha) \neq 0$ if and only if $q \neq 0$ in $\mathbb{Q}_{\geq 0}$.

NNRat.cast_add theorem

(p q : ℚ≥0) : ↑(p + q) = (p + q : α)

Full source

@[simp, norm_cast] lemma cast_add (p q : ℚ≥0) : ↑(p + q) = (p + q : α) :=
  cast_add_of_ne_zero (Nat.cast_ne_zero.2 p.den_pos.ne') (Nat.cast_ne_zero.2 q.den_pos.ne')

Addition Preservation under Canonical Map from Nonnegative Rationals to Characteristic Zero Field

Informal description

For any nonnegative rational numbers $p$ and $q$, the canonical map from nonnegative rationals to a characteristic zero field (or division ring) $\alpha$ preserves addition, i.e., $(p + q) = (p : \alpha) + (q : \alpha)$.

NNRat.cast_mul theorem

(p q) : (p * q : ℚ≥0) = (p * q : α)

Full source

@[simp, norm_cast] lemma cast_mul (p q) : (p * q : ℚ≥0) = (p * q : α) :=
  cast_mul_of_ne_zero (Nat.cast_ne_zero.2 p.den_pos.ne') (Nat.cast_ne_zero.2 q.den_pos.ne')

Multiplication Preservation in Nonnegative Rationals Cast

Informal description

For any nonnegative rational numbers $p$ and $q$, the canonical map from nonnegative rationals to a characteristic zero field (or division ring) $\alpha$ preserves multiplication, i.e., $(p \cdot q) = (p \cdot q : \alpha)$.

NNRat.castHom definition

: ℚ≥0 →+* α

Full source

/-- Coercion `ℚ≥0 → α` as a `RingHom`. -/
def castHom : ℚ≥0ℚ≥0 →+* α where
  toFun := (↑)
  map_one' := cast_one
  map_mul' := cast_mul
  map_zero' := cast_zero
  map_add' := cast_add

Ring homomorphism from nonnegative rationals to a characteristic zero field

Informal description

The function `NNRat.castHom` is a ring homomorphism from the nonnegative rationals $\mathbb{Q}_{\geq 0}$ to a characteristic zero field (or division ring) $\alpha$, defined by the canonical inclusion map. It satisfies: - $1$ maps to $1$, - $0$ maps to $0$, - addition is preserved: $(p + q) = (p : \alpha) + (q : \alpha)$, - multiplication is preserved: $(p \cdot q) = (p \cdot q : \alpha)$.

NNRat.coe_castHom theorem

: ⇑(castHom α) = (↑)

Full source

@[simp, norm_cast] lemma coe_castHom : ⇑(castHom α) = (↑) := rfl

Underlying Function of Nonnegative Rationals Ring Homomorphism Equals Canonical Inclusion

Informal description

The underlying function of the ring homomorphism `NNRat.castHom` from nonnegative rationals to a characteristic zero field (or division ring) $\alpha$ is equal to the canonical inclusion map $\mathbb{Q}_{\geq 0} \hookrightarrow \alpha$.

NNRat.cast_inv theorem

(p) : (p⁻¹ : ℚ≥0) = (p : α)⁻¹

Full source

@[simp, norm_cast] lemma cast_inv (p) : (p⁻¹ : ℚ≥0) = (p : α)⁻¹ := map_inv₀ (castHom α) _

Preservation of Inversion under Canonical Map from Nonnegative Rationals to Characteristic Zero Fields

Informal description

For any nonnegative rational number $p \in \mathbb{Q}_{\geq 0}$, the canonical map from $\mathbb{Q}_{\geq 0}$ to a characteristic zero field (or division ring) $\alpha$ preserves inversion, i.e., $(p^{-1} : \alpha) = (p : \alpha)^{-1}$.

NNRat.cast_div theorem

(p q) : (p / q : ℚ≥0) = (p / q : α)

Full source

@[simp, norm_cast] lemma cast_div (p q) : (p / q : ℚ≥0) = (p / q : α) := map_div₀ (castHom α) ..

Preservation of Division under Canonical Map from Nonnegative Rationals to Characteristic Zero Fields

Informal description

For any nonnegative rational numbers $p$ and $q$, the canonical map from $\mathbb{Q}_{\geq 0}$ to a characteristic zero field (or division ring) $\alpha$ preserves division, i.e., $(p / q : \alpha) = (p : \alpha) / (q : \alpha)$.

NNRat.cast_zpow theorem

(q : ℚ≥0) (p : ℤ) : ↑(q ^ p) = ((q : α) ^ p : α)

Full source

@[simp, norm_cast]
lemma cast_zpow (q : ℚ≥0) (p : ℤ) : ↑(q ^ p) = ((q : α) ^ p : α) := map_zpow₀ (castHom α) ..

Preservation of Integer Powers under Canonical Map from Nonnegative Rationals to Characteristic Zero Fields

Informal description

For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$ and any integer exponent $p \in \mathbb{Z}$, the canonical map from nonnegative rationals to a characteristic zero field (or division ring) $\alpha$ preserves integer powers, i.e., $(q^p : \alpha) = (q : \alpha)^p$.

NNRat.cast_divNat theorem

(a b : ℕ) : (divNat a b : α) = a / b

Full source

@[simp]
lemma cast_divNat (a b : ℕ) : (divNat a b : α) = a / b := by
  rw [← cast_natCast, ← cast_natCast b, ← cast_div]
  congr
  ext
  apply Rat.mkRat_eq_div

Preservation of Natural Number Division under Canonical Map to Characteristic Zero Fields

Informal description

For any natural numbers $a$ and $b$, the canonical map from nonnegative rationals to a characteristic zero field (or division ring) $\alpha$ preserves division of natural numbers, i.e., $(a / b : \alpha) = (a : \alpha) / (b : \alpha)$.