Mathlib.Data.Int.Cast.Field

Module docstring

{"# Cast of integers into fields

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

Main results

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

Int.cast_neg_natCast theorem

{R} [DivisionRing R] (n : ℕ) : ((-n : ℤ) : R) = -n

Full source

/-- Auxiliary lemma for norm_cast to move the cast `-↑n` upwards to `↑-↑n`.

(The restriction to `DivisionRing` is necessary, otherwise this would also apply in the case where
`R = ℤ` and cause nontermination.)
-/
@[norm_cast]
theorem cast_neg_natCast {R} [DivisionRing R] (n : ℕ) : ((-n : ℤ) : R) = -n := by simp

Negation Preserved Under Integer-to-Division-Ring Cast

Informal description

Let $R$ be a division ring. For any natural number $n$, the canonical homomorphism from $\mathbb{Z}$ to $R$ satisfies $(-n) = -n$ in $R$.

Int.cast_div theorem

[DivisionRing α] {m n : ℤ} (n_dvd : n ∣ m) (hn : (n : α) ≠ 0) : ((m / n : ℤ) : α) = m / n

Full source

@[simp]
theorem cast_div [DivisionRing α] {m n : ℤ} (n_dvd : n ∣ m) (hn : (n : α) ≠ 0) :
    ((m / n : ℤ) : α) = m / n := by
  rcases n_dvd with ⟨k, rfl⟩
  have : n ≠ 0 := by rintro rfl; simp at hn
  rw [Int.mul_ediv_cancel_left _ this, mul_comm n, Int.cast_mul, mul_div_cancel_right₀ _ hn]

Canonical Homomorphism Preserves Integer Division in Division Rings

Informal description

Let $\alpha$ be a division ring. For any integers $m$ and $n$ such that $n$ divides $m$ and the image of $n$ in $\alpha$ is nonzero, the canonical homomorphism from $\mathbb{Z}$ to $\alpha$ satisfies $\left(\frac{m}{n}\right) = \frac{m}{n}$ in $\alpha$.