Mathlib.Data.Int.CharZero

Int.cast_div_charZero theorem

{k : Type*} [DivisionRing k] [CharZero k] {m n : ℤ} (n_dvd : n ∣ m) : ((m / n : ℤ) : k) = m / n

Full source

@[simp, norm_cast]
theorem cast_div_charZero {k : Type*} [DivisionRing k] [CharZero k] {m n : ℤ} (n_dvd : n ∣ m) :
    ((m / n : ℤ) : k) = m / n := by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp [Int.ediv_zero]
  · exact cast_div n_dvd (cast_ne_zero.mpr hn)

Canonical Homomorphism Preserves Integer Division in Characteristic Zero Division Rings

Informal description

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

Int.cast_div_ofNat_charZero theorem

{k : Type*} [DivisionRing k] [CharZero k] {m n : ℕ} (n_dvd : n ∣ m) : (((m : ℤ) / (n : ℤ) : ℤ) : k) = m / n

Full source

@[simp, norm_cast]
theorem cast_div_ofNat_charZero {k : Type*} [DivisionRing k] [CharZero k] {m n : ℕ}
    (n_dvd : n ∣ m) : (((m : ℤ) / (n : ℤ) : ℤ) : k) = m / n := by
  rw [cast_div_charZero (Int.ofNat_dvd.mpr n_dvd), cast_natCast, cast_natCast]

Canonical Homomorphism Preserves Natural Number Division in Characteristic Zero Division Rings

Informal description

Let $k$ be a division ring of characteristic zero. For any natural numbers $m$ and $n$ such that $n$ divides $m$, the canonical homomorphism from the integers to $k$ satisfies $\left(\frac{m}{n}\right) = \frac{m}{n}$ in $k$, where the division on the left is integer division and the division on the right is in $k$.

RingHom.injective_int theorem

{α : Type*} [NonAssocRing α] (f : ℤ →+* α) [CharZero α] : Function.Injective f

Full source

theorem RingHom.injective_int {α : Type*} [NonAssocRing α] (f : ℤℤ →+* α) [CharZero α] :
    Function.Injective f :=
  Subsingleton.elim (Int.castRingHom _) f ▸ Int.cast_injective

Injectivity of Ring Homomorphisms from Integers to Characteristic Zero Rings

Informal description

Let $\alpha$ be a non-associative ring of characteristic zero. Then any ring homomorphism $f \colon \mathbb{Z} \to \alpha$ is injective.

Function.support_intCast theorem

(hn : n ≠ 0) : support (n : α → β) = univ

Full source

lemma support_intCast (hn : n ≠ 0) : support (n : α → β) = univ :=
  support_const <| Int.cast_ne_zero.2 hn

Support of Nonzero Integer Constant Function is Universal Set

Informal description

For any integer $n \neq 0$ and any function type $\alpha \to \beta$, the support of the constant function $n$ (i.e., the set of points where $n$ is nonzero) is equal to the universal set $\alpha$.

Function.mulSupport_intCast theorem

(hn : n ≠ 1) : mulSupport (n : α → β) = univ

Full source

lemma mulSupport_intCast (hn : n ≠ 1) : mulSupport (n : α → β) = univ :=
  mulSupport_const <| Int.cast_ne_one.2 hn

Multiplicative Support of Non-Identity Integer Constant Function is Universal Set

Informal description

For any integer $n \neq 1$ and any function type $\alpha \to \beta$, the multiplicative support of the constant function $n$ (i.e., the set of points where $n$ is not equal to the multiplicative identity $1$) is equal to the universal set $\alpha$.