Mathlib.Data.Nat.Cast.Field

Module docstring

{"# Cast of naturals into fields

This file concerns the canonical homomorphism ℕ → F, where F is a field.

Main results

Nat.cast_div: if n divides m, then ↑(m / n) = ↑m / ↑n "}

Nat.cast_div theorem

(hnm : n ∣ m) (hn : (n : K) ≠ 0) : (↑(m / n) : K) = m / n

Full source

@[simp]
lemma cast_div (hnm : n ∣ m) (hn : (n : K) ≠ 0) : (↑(m / n) : K) = m / n := by
  obtain ⟨k, rfl⟩ := hnm
  have : n ≠ 0 := by rintro rfl; simp at hn
  rw [Nat.mul_div_cancel_left _ <| zero_lt_of_ne_zero this, mul_comm n,
    cast_mul, mul_div_cancel_right₀ _ hn]

Canonical homomorphism preserves division of natural numbers in fields

Informal description

Let $K$ be a field and let $n, m$ be natural numbers such that $n$ divides $m$ and the canonical image of $n$ in $K$ is nonzero. Then the canonical image of the natural number division $m / n$ in $K$ equals the field division of the canonical images of $m$ and $n$ in $K$, i.e., $\uparrow(m / n) = \uparrow m / \uparrow n$.

Nat.cast_div_charZero theorem

(hnm : n ∣ m) : (↑(m / n) : K) = m / n

Full source

@[simp, norm_cast]
lemma cast_div_charZero (hnm : n ∣ m) : (↑(m / n) : K) = m / n := by
  obtain rfl | hn := eq_or_ne n 0 <;> simp [*]

Characteristic Zero Field Preserves Natural Division under Canonical Homomorphism

Informal description

Let $K$ be a field of characteristic zero and let $n, m$ be natural numbers such that $n$ divides $m$. Then the canonical image of the natural number division $m / n$ in $K$ equals the field division of the canonical images of $m$ and $n$ in $K$, i.e., $(m / n) = m / n$ (where the left side is the natural number division and the right side is the field division).

Nat.cast_div_div_div_cancel_right theorem

(hn : d ∣ n) (hm : d ∣ m) : (↑(m / d) : K) / (↑(n / d) : K) = (m : K) / n

Full source

lemma cast_div_div_div_cancel_right (hn : d ∣ n) (hm : d ∣ m) :
    (↑(m / d) : K) / (↑(n / d) : K) = (m : K) / n := by
  rcases eq_or_ne d 0 with (rfl | hd); · simp [Nat.zero_dvd.1 hm]
  replace hd : (d : K) ≠ 0 := by norm_cast
  rw [cast_div hm, cast_div hn, div_div_div_cancel_right₀ hd] <;> exact hd

Cancellation of Common Divisor in Field Division of Natural Number Casts

Informal description

Let $K$ be a field of characteristic zero, and let $d, m, n$ be natural numbers such that $d$ divides both $m$ and $n$. Then the division of the canonical images of $m/d$ and $n/d$ in $K$ equals the division of the canonical images of $m$ and $n$ in $K$, i.e., \[ \frac{\uparrow(m/d)}{\uparrow(n/d)} = \frac{\uparrow m}{\uparrow n}. \]