Mathlib.Data.Rat.Cast.Defs

NNRat.cast_natCast theorem

(n : ℕ) : ((n : ℚ≥0) : α) = n

Full source

@[simp, norm_cast] lemma cast_natCast (n : ℕ) : ((n : ℚ≥0) : α) = n := by simp [cast_def]

Natural Number Cast Consistency for Non-Negative Rationals

Informal description

For any natural number $n$ and any division ring $\alpha$, the canonical map from non-negative rational numbers to $\alpha$ maps the natural number $n$ (viewed as a non-negative rational) to $n$ in $\alpha$, i.e., $(n : \mathbb{Q}_{\geq 0}) = (n : \alpha)$.

NNRat.cast_ofNat theorem

(n : ℕ) [n.AtLeastTwo] : (ofNat(n) : ℚ≥0) = (ofNat(n) : α)

Full source

@[simp, norm_cast] lemma cast_ofNat (n : ℕ) [n.AtLeastTwo] :
    (ofNat(n) : ℚ≥0) = (ofNat(n) : α) := cast_natCast _

Numeral Cast Consistency for Non-Negative Rationals: $(n : \mathbb{Q}_{\geq 0}) = (n : \alpha)$ for $n \geq 2$

Informal description

For any natural number $n \geq 2$ and any division ring $\alpha$, the canonical injection from non-negative rational numbers to $\alpha$ maps the numeral $n$ (viewed as a non-negative rational) to $n$ in $\alpha$, i.e., $(n : \mathbb{Q}_{\geq 0}) = (n : \alpha)$.

NNRat.cast_zero theorem

: ((0 : ℚ≥0) : α) = 0

Full source

@[simp, norm_cast] lemma cast_zero : ((0 : ℚ≥0) : α) = 0 := (cast_natCast _).trans Nat.cast_zero

Preservation of Additive Identity in Non-Negative Rational Cast

Informal description

The canonical injection from the non-negative rational numbers $\mathbb{Q}_{\geq 0}$ to a division ring $\alpha$ maps the additive identity $0 \in \mathbb{Q}_{\geq 0}$ to the additive identity $0 \in \alpha$, i.e., $(0 : \mathbb{Q}_{\geq 0}) = (0 : \alpha)$.

NNRat.cast_one theorem

: ((1 : ℚ≥0) : α) = 1

Full source

@[simp, norm_cast] lemma cast_one : ((1 : ℚ≥0) : α) = 1 := (cast_natCast _).trans Nat.cast_one

Preservation of Multiplicative Identity in Non-Negative Rational Cast

Informal description

The canonical injection from the non-negative rational numbers $\mathbb{Q}_{\geq 0}$ to a division ring $\alpha$ maps the multiplicative identity $1 \in \mathbb{Q}_{\geq 0}$ to the multiplicative identity $1 \in \alpha$, i.e., $(1 : \mathbb{Q}_{\geq 0}) = (1 : \alpha)$.

NNRat.cast_commute theorem

(q : ℚ≥0) (a : α) : Commute (↑q) a

Full source

lemma cast_commute (q : ℚ≥0) (a : α) : Commute (↑q) a := by
  simpa only [cast_def] using (q.num.cast_commute a).div_left (q.den.cast_commute a)

Commutation of Nonnegative Rational Cast with Ring Elements

Informal description

For any nonnegative rational number $q$ and any element $a$ in a division ring $\alpha$, the elements $q$ (viewed as an element of $\alpha$ via the canonical injection) and $a$ commute under multiplication, i.e., $q \cdot a = a \cdot q$.

NNRat.commute_cast theorem

(a : α) (q : ℚ≥0) : Commute a q

Full source

lemma commute_cast (a : α) (q : ℚ≥0) : Commute a q := (cast_commute ..).symm

Commutation of Ring Elements with Nonnegative Rational Cast

Informal description

For any element $a$ in a division ring $\alpha$ and any nonnegative rational number $q$, the elements $a$ and $q$ (viewed as an element of $\alpha$ via the canonical injection) commute under multiplication, i.e., $a \cdot q = q \cdot a$.

NNRat.cast_comm theorem

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

Full source

lemma cast_comm (q : ℚ≥0) (a : α) : q * a = a * q := cast_commute _ _

Commutativity of Nonnegative Rational Cast with Ring Elements

Informal description

For any nonnegative rational number $q$ and any element $a$ in a division ring $\alpha$, the multiplication of $q$ (viewed as an element of $\alpha$ via the canonical injection) and $a$ commutes, i.e., $q \cdot a = a \cdot q$.

NNRat.cast_divNat_of_ne_zero theorem

(a : ℕ) {b : ℕ} (hb : (b : α) ≠ 0) : divNat a b = (a / b : α)

Full source

@[norm_cast] lemma cast_divNat_of_ne_zero (a : ℕ) {b : ℕ} (hb : (b : α) ≠ 0) :
    divNat a b = (a / b : α) := by
  rcases e : divNat a b with ⟨⟨n, d, h, c⟩, hn⟩
  rw [← Rat.num_nonneg] at hn
  lift n to ℕ using hn
  have hd : (d : α) ≠ 0 := by
    refine fun hd ↦ hb ?_
    have : Rat.divInt a b = _ := congr_arg NNRat.cast e
    obtain ⟨k, rfl⟩ : d ∣ b := by simpa [Int.natCast_dvd_natCast, this] using Rat.den_dvd a b
    simp [*]
  have hb' : b ≠ 0 := by rintro rfl; exact hb Nat.cast_zero
  have hd' : d ≠ 0 := by rintro rfl; exact hd Nat.cast_zero
  simp_rw [Rat.mk'_eq_divInt, mk_divInt, divNat_inj hb' hd'] at e
  rw [cast_def]
  dsimp
  rw [Commute.div_eq_div_iff _ hd hb]
  · norm_cast
    rw [e]
  exact b.commute_cast _

Canonical Injection Preserves Division for Nonzero Denominator

Informal description

For any natural numbers $a$ and $b$, if the image of $b$ in a division ring $\alpha$ is nonzero (i.e., $(b : \alpha) \neq 0$), then the canonical injection of the rational number $\mathrm{divNat}(a, b)$ (defined as $a/b$ in $\mathbb{Q}$) into $\alpha$ equals the division of the images of $a$ and $b$ in $\alpha$, i.e., $\mathrm{divNat}(a, b) = (a : \alpha) / (b : \alpha)$.

NNRat.cast_add_of_ne_zero theorem

(hq : (q.den : α) ≠ 0) (hr : (r.den : α) ≠ 0) : ↑(q + r) = (q + r : α)

Full source

@[norm_cast]
lemma cast_add_of_ne_zero (hq : (q.den : α) ≠ 0) (hr : (r.den : α) ≠ 0) :
    ↑(q + r) = (q + r : α) := by
  rw [add_def, cast_divNat_of_ne_zero, cast_def, cast_def, mul_comm _ q.den,
    (Nat.commute_cast _ _).div_add_div (Nat.commute_cast _ _) hq hr]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hq hr

Canonical Injection Preserves Addition for Nonzero Denominators

Informal description

For any nonnegative rational numbers $q$ and $r$ in $\mathbb{Q}_{\geq 0}$, if the denominators of $q$ and $r$ are nonzero when cast into a division ring $\alpha$ (i.e., $(q.den : \alpha) \neq 0$ and $(r.den : \alpha) \neq 0$), then the canonical injection of their sum into $\alpha$ equals the sum of their injections, i.e., $(q + r : \alpha) = (q : \alpha) + (r : \alpha)$.

NNRat.cast_mul_of_ne_zero theorem

(hq : (q.den : α) ≠ 0) (hr : (r.den : α) ≠ 0) : ↑(q * r) = (q * r : α)

Full source

@[norm_cast]
lemma cast_mul_of_ne_zero (hq : (q.den : α) ≠ 0) (hr : (r.den : α) ≠ 0) :
    ↑(q * r) = (q * r : α) := by
  rw [mul_def, cast_divNat_of_ne_zero, cast_def, cast_def,
    (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hq hr

Canonical Injection Preserves Multiplication for Nonzero Denominators

Informal description

For any nonnegative rational numbers $q$ and $r$ and any division ring $\alpha$, if the images of the denominators of $q$ and $r$ in $\alpha$ are nonzero (i.e., $(q.\text{den} : \alpha) \neq 0$ and $(r.\text{den} : \alpha) \neq 0$), then the canonical injection of the product $q \cdot r$ into $\alpha$ equals the product of the images of $q$ and $r$ in $\alpha$, i.e., $(q \cdot r : \alpha) = (q : \alpha) \cdot (r : \alpha)$.

NNRat.cast_inv_of_ne_zero theorem

(hq : (q.num : α) ≠ 0) : (q⁻¹ : ℚ≥0) = (q⁻¹ : α)

Full source

@[norm_cast]
lemma cast_inv_of_ne_zero (hq : (q.num : α) ≠ 0) : (q⁻¹ : ℚ≥0) = (q⁻¹ : α) := by
  rw [inv_def, cast_divNat_of_ne_zero _ hq, cast_def, inv_div]

Canonical Injection Preserves Inverse for Nonzero Numerator

Informal description

For any nonnegative rational number $q$ and any division ring $\alpha$, if the image of the numerator of $q$ in $\alpha$ is nonzero (i.e., $(q.\mathrm{num} : \alpha) \neq 0$), then the canonical injection of the inverse of $q$ into $\alpha$ equals the inverse of the image of $q$ in $\alpha$, i.e., $(q^{-1} : \mathbb{Q}_{\geq 0}) = (q : \alpha)^{-1}$.

NNRat.cast_div_of_ne_zero theorem

(hq : (q.den : α) ≠ 0) (hr : (r.num : α) ≠ 0) : ↑(q / r) = (q / r : α)

Full source

@[norm_cast]
lemma cast_div_of_ne_zero (hq : (q.den : α) ≠ 0) (hr : (r.num : α) ≠ 0) :
    ↑(q / r) = (q / r : α) := by
  rw [div_def, cast_divNat_of_ne_zero, cast_def, cast_def, div_eq_mul_inv (_ / _),
    inv_div, (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hq hr

Canonical Injection Preserves Division for Nonzero Denominator and Numerator in Nonnegative Rationals

Informal description

For any nonnegative rational numbers $q$ and $r$ in $\mathbb{Q}_{\geq 0}$, if the image of the denominator of $q$ in a division ring $\alpha$ is nonzero (i.e., $(q.\text{den} : \alpha) \neq 0$) and the image of the numerator of $r$ in $\alpha$ is nonzero (i.e., $(r.\text{num} : \alpha) \neq 0$), then the canonical injection of the quotient $q / r$ into $\alpha$ equals the division of the images of $q$ and $r$ in $\alpha$, i.e., $(q / r : \alpha) = (q : \alpha) / (r : \alpha)$.

Rat.cast_intCast theorem

(n : ℤ) : ((n : ℚ) : α) = n

Full source

@[simp, norm_cast]
theorem cast_intCast (n : ℤ) : ((n : ℚ) : α) = n :=
  (cast_def _).trans <| show (n / (1 : ℕ) : α) = n by rw [Nat.cast_one, div_one]

Compatibility of Integer Casts with Rational and Division Ring Injections: $(n : \mathbb{Q}) : \alpha = n$

Informal description

For any integer $n$ and any division ring $\alpha$, the canonical injection of $n$ into the rational numbers $\mathbb{Q}$ followed by the canonical injection into $\alpha$ equals the direct injection of $n$ into $\alpha$, i.e., $(n : \mathbb{Q}) : \alpha = n$.

Rat.cast_natCast theorem

(n : ℕ) : ((n : ℚ) : α) = n

Full source

@[simp, norm_cast]
theorem cast_natCast (n : ℕ) : ((n : ℚ) : α) = n := by
  rw [← Int.cast_natCast, cast_intCast, Int.cast_natCast]

Compatibility of Natural Number Casts with Rational and Division Ring Injections: $(n : \mathbb{Q}) : \alpha = n$

Informal description

For any natural number $n$ and any division ring $\alpha$, the canonical injection of $n$ into the rational numbers $\mathbb{Q}$ followed by the canonical injection into $\alpha$ equals the direct injection of $n$ into $\alpha$, i.e., $(n : \mathbb{Q}) : \alpha = n$.

Rat.cast_ofNat theorem

(n : ℕ) [n.AtLeastTwo] : ((ofNat(n) : ℚ) : α) = (ofNat(n) : α)

Full source

@[simp, norm_cast] lemma cast_ofNat (n : ℕ) [n.AtLeastTwo] :
    ((ofNat(n) : ℚ) : α) = (ofNat(n) : α) := by
  simp [cast_def]

Canonical Injection of Numeric Literals from Rationals to Division Rings

Informal description

For any natural number $n \geq 2$ and any division ring $\alpha$, the canonical injection of the rational number $\mathrm{ofNat}(n)$ into $\alpha$ equals the canonical injection of $n$ into $\alpha$ directly, i.e., $(\mathrm{ofNat}(n) : \mathbb{Q}) : \alpha = (\mathrm{ofNat}(n) : \alpha)$.

Rat.cast_zero theorem

: ((0 : ℚ) : α) = 0

Full source

@[simp, norm_cast]
theorem cast_zero : ((0 : ℚ) : α) = 0 :=
  (cast_intCast _).trans Int.cast_zero

Zero Preservation in Rational Number Cast: $(0 : \mathbb{Q}) : \alpha = 0$

Informal description

The canonical injection of the rational number $0$ into a division ring $\alpha$ equals the zero element of $\alpha$, i.e., $(0 : \mathbb{Q}) : \alpha = 0$.

Rat.cast_one theorem

: ((1 : ℚ) : α) = 1

Full source

@[simp, norm_cast]
theorem cast_one : ((1 : ℚ) : α) = 1 :=
  (cast_intCast _).trans Int.cast_one

One Preservation in Rational Number Cast: $(1 : \mathbb{Q}) : \alpha = 1$

Informal description

The canonical injection of the rational number $1$ into a division ring $\alpha$ equals the multiplicative identity element of $\alpha$, i.e., $(1 : \mathbb{Q}) : \alpha = 1$.

Rat.cast_commute theorem

(r : ℚ) (a : α) : Commute (↑r) a

Full source

theorem cast_commute (r : ℚ) (a : α) : Commute (↑r) a := by
  simpa only [cast_def] using (r.1.cast_commute a).div_left (r.2.cast_commute a)

Commutativity of Rational Number Cast in Division Ring

Informal description

For any rational number $r$ and any element $a$ in a division ring $\alpha$, the cast of $r$ into $\alpha$ commutes with $a$, i.e., $r \cdot a = a \cdot r$.

Rat.cast_comm theorem

(r : ℚ) (a : α) : (r : α) * a = a * r

Full source

theorem cast_comm (r : ℚ) (a : α) : (r : α) * a = a * r :=
  (cast_commute r a).eq

Commutativity of Rational Cast Multiplication in Division Ring

Informal description

For any rational number $r$ and any element $a$ in a division ring $\alpha$, the canonical injection of $r$ into $\alpha$ satisfies $(r : \alpha) \cdot a = a \cdot (r : \alpha)$.

Rat.commute_cast theorem

(a : α) (r : ℚ) : Commute a r

Full source

theorem commute_cast (a : α) (r : ℚ) : Commute a r :=
  (r.cast_commute a).symm

Commutativity of Element with Rational Cast in Division Ring

Informal description

For any element $a$ in a division ring $\alpha$ and any rational number $r$, the element $a$ commutes with the cast of $r$ into $\alpha$, i.e., $a \cdot r = r \cdot a$.

Rat.cast_divInt_of_ne_zero theorem

(a : ℤ) {b : ℤ} (b0 : (b : α) ≠ 0) : (a /. b : α) = a / b

Full source

@[norm_cast]
lemma cast_divInt_of_ne_zero (a : ℤ) {b : ℤ} (b0 : (b : α) ≠ 0) : (a /. b : α) = a / b := by
  have b0' : b ≠ 0 := by
    refine mt ?_ b0
    simp +contextual
  rcases e : a /. b with ⟨n, d, h, c⟩
  have d0 : (d : α) ≠ 0 := by
    intro d0
    have dd := den_dvd a b
    rcases show (d : ℤ) ∣ b by rwa [e] at dd with ⟨k, ke⟩
    have : (b : α) = (d : α) * (k : α) := by rw [ke, Int.cast_mul, Int.cast_natCast]
    rw [d0, zero_mul] at this
    contradiction
  rw [mk'_eq_divInt] at e
  have := congr_arg ((↑) : ℤ → α)
    ((divInt_eq_iff b0' <| ne_of_gt <| Int.natCast_pos.2 h.bot_lt).1 e)
  rw [Int.cast_mul, Int.cast_mul, Int.cast_natCast] at this
  rw [eq_comm, cast_def, div_eq_mul_inv, eq_div_iff_mul_eq d0, mul_assoc, (d.commute_cast _).eq,
    ← mul_assoc, this, mul_assoc, mul_inv_cancel₀ b0, mul_one]

Rational Cast as Division in Division Ring

Informal description

For any integer $a$ and any integer $b$ such that the canonical injection of $b$ into a division ring $\alpha$ is nonzero (i.e., $(b : \alpha) \neq 0$), the canonical injection of the rational number $a /. b$ into $\alpha$ equals the division of $a$ by $b$ in $\alpha$, i.e., $(a /. b : \alpha) = a / b$.

Rat.cast_mkRat_of_ne_zero theorem

(a : ℤ) {b : ℕ} (hb : (b : α) ≠ 0) : (mkRat a b : α) = a / b

Full source

@[norm_cast]
lemma cast_mkRat_of_ne_zero (a : ℤ) {b : ℕ} (hb : (b : α) ≠ 0) : (mkRat a b : α) = a / b := by
  rw [Rat.mkRat_eq_divInt, cast_divInt_of_ne_zero, Int.cast_natCast]; rwa [Int.cast_natCast]

Rational Construction Cast as Division in Division Ring

Informal description

For any integer $a$ and any natural number $b$ such that the canonical injection of $b$ into a division ring $\alpha$ is nonzero (i.e., $(b : \alpha) \neq 0$), the canonical injection of the rational number $\text{mkRat}(a, b)$ into $\alpha$ equals the division of $a$ by $b$ in $\alpha$, i.e., $(\text{mkRat}(a, b) : \alpha) = a / b$.

Rat.cast_add_of_ne_zero theorem

{q r : ℚ} (hq : (q.den : α) ≠ 0) (hr : (r.den : α) ≠ 0) : (q + r : ℚ) = (q + r : α)

Full source

@[norm_cast]
lemma cast_add_of_ne_zero {q r : ℚ} (hq : (q.den : α) ≠ 0) (hr : (r.den : α) ≠ 0) :
    (q + r : ℚ) = (q + r : α) := by
  rw [add_def', cast_mkRat_of_ne_zero, cast_def, cast_def, mul_comm r.num,
    (Nat.cast_commute _ _).div_add_div (Nat.commute_cast _ _) hq hr]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hq hr

Addition Commutes with Rational Number Casting in Division Rings

Informal description

For any rational numbers $q$ and $r$ in a division ring $\alpha$, if the denominators of $q$ and $r$ are nonzero in $\alpha$ (i.e., $(q.\text{den} : \alpha) \neq 0$ and $(r.\text{den} : \alpha) \neq 0$), then the canonical injection of $q + r$ into $\alpha$ equals the sum of the canonical injections of $q$ and $r$ into $\alpha$, i.e., $(q + r : \alpha) = (q : \alpha) + (r : \alpha)$.

Rat.cast_neg theorem

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

Full source

@[simp, norm_cast] lemma cast_neg (q : ℚ) : ↑(-q) = (-q : α) := by simp [cast_def, neg_div]

Negation Commutes with Rational Number Casting

Informal description

For any rational number $q$, the canonical injection of $-q$ into a division ring $\alpha$ equals the negation of the canonical injection of $q$ into $\alpha$, i.e., $(-q : \alpha) = - (q : \alpha)$.

Rat.cast_sub_of_ne_zero theorem

(hp : (p.den : α) ≠ 0) (hq : (q.den : α) ≠ 0) : ↑(p - q) = (p - q : α)

Full source

@[norm_cast] lemma cast_sub_of_ne_zero (hp : (p.den : α) ≠ 0) (hq : (q.den : α) ≠ 0) :
    ↑(p - q) = (p - q : α) := by simp [sub_eq_add_neg, cast_add_of_ne_zero, hp, hq]

Subtraction Commutes with Rational Number Casting in Division Rings

Informal description

For any rational numbers $p$ and $q$ in a division ring $\alpha$, if the denominators of $p$ and $q$ are nonzero in $\alpha$ (i.e., $(p.\text{den} : \alpha) \neq 0$ and $(q.\text{den} : \alpha) \neq 0$), then the canonical injection of $p - q$ into $\alpha$ equals the difference of the canonical injections of $p$ and $q$ into $\alpha$, i.e., $(p - q : \alpha) = (p : \alpha) - (q : \alpha)$.

Rat.cast_mul_of_ne_zero theorem

(hp : (p.den : α) ≠ 0) (hq : (q.den : α) ≠ 0) : ↑(p * q) = (p * q : α)

Full source

@[norm_cast] lemma cast_mul_of_ne_zero (hp : (p.den : α) ≠ 0) (hq : (q.den : α) ≠ 0) :
    ↑(p * q) = (p * q : α) := by
  rw [mul_eq_mkRat, cast_mkRat_of_ne_zero, cast_def, cast_def,
    (Nat.commute_cast _ _).div_mul_div_comm (Int.commute_cast _ _)]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hp hq

Multiplication Commutes with Rational Number Casting in Division Rings

Informal description

For any rational numbers $p$ and $q$ in a division ring $\alpha$, if the denominators of $p$ and $q$ are nonzero in $\alpha$ (i.e., $(p.\text{den} : \alpha) \neq 0$ and $(q.\text{den} : \alpha) \neq 0$), then the canonical injection of the product $p \cdot q$ into $\alpha$ equals the product of the canonical injections of $p$ and $q$ into $\alpha$, i.e., $(p \cdot q : \alpha) = (p : \alpha) \cdot (q : \alpha)$.

Rat.cast_inv_of_ne_zero theorem

(hq : (q.num : α) ≠ 0) : ↑(q⁻¹) = (q⁻¹ : α)

Full source

@[norm_cast]
lemma cast_inv_of_ne_zero (hq : (q.num : α) ≠ 0) : ↑(q⁻¹) = (q⁻¹ : α) := by
  rw [inv_def', cast_divInt_of_ne_zero _ hq, cast_def, inv_div, Int.cast_natCast]

Inverse of Rational Number Cast Equals Cast of Inverse

Informal description

For any rational number $q$ and any division ring $\alpha$, if the canonical injection of the numerator of $q$ into $\alpha$ is nonzero (i.e., $(q.\text{num} : \alpha) \neq 0$), then the canonical injection of the inverse of $q$ into $\alpha$ equals the inverse of the canonical injection of $q$ into $\alpha$, i.e., $(q^{-1} : \alpha) = (q : \alpha)^{-1}$.

Rat.cast_div_of_ne_zero theorem

(hp : (p.den : α) ≠ 0) (hq : (q.num : α) ≠ 0) : ↑(p / q) = (p / q : α)

Full source

@[norm_cast] lemma cast_div_of_ne_zero (hp : (p.den : α) ≠ 0) (hq : (q.num : α) ≠ 0) :
    ↑(p / q) = (p / q : α) := by
  rw [div_def', cast_divInt_of_ne_zero, cast_def, cast_def, div_eq_mul_inv (_ / _), inv_div,
    (Int.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hp hq

Canonical Injection of Rational Division in Division Ring

Informal description

For any rational numbers $p$ and $q$ in a division ring $\alpha$, if the denominator of $p$ is nonzero in $\alpha$ (i.e., $(p.\text{den} : \alpha) \neq 0$) and the numerator of $q$ is nonzero in $\alpha$ (i.e., $(q.\text{num} : \alpha) \neq 0$), then the canonical injection of the quotient $p / q$ into $\alpha$ equals the division of $p$ by $q$ in $\alpha$, i.e., $(p / q : \alpha) = (p : \alpha) / (q : \alpha)$.

map_nnratCast theorem

[DivisionSemiring α] [DivisionSemiring β] [RingHomClass F α β] (f : F) (q : ℚ≥0) : f q = q

Full source

@[simp] lemma map_nnratCast [DivisionSemiring α] [DivisionSemiring β] [RingHomClass F α β] (f : F)
    (q : ℚ≥0) : f q = q := by simp_rw [NNRat.cast_def, map_div₀, map_natCast]

Preservation of Nonnegative Rational Numbers under Ring Homomorphisms

Informal description

Let $\alpha$ and $\beta$ be division semirings, and let $F$ be a type of ring homomorphisms from $\alpha$ to $\beta$. For any ring homomorphism $f \in F$ and any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the image of $q$ under $f$ is equal to $q$ itself, i.e., $f(q) = q$.

map_ratCast theorem

[DivisionRing α] [DivisionRing β] [RingHomClass F α β] (f : F) (q : ℚ) : f q = q

Full source

@[simp]
theorem map_ratCast [DivisionRing α] [DivisionRing β] [RingHomClass F α β] (f : F) (q : ℚ) :
    f q = q := by rw [cast_def, map_div₀, map_intCast, map_natCast, cast_def]

Rational Number Preservation under Ring Homomorphisms between Division Rings

Informal description

Let $\alpha$ and $\beta$ be division rings, and let $F$ be a type of ring homomorphisms from $\alpha$ to $\beta$. For any ring homomorphism $f \in F$ and any rational number $q \in \mathbb{Q}$, the image of $q$ under $f$ is equal to $q$ itself, i.e., $f(q) = q$.

MonoidWithZeroHomClass.ext_nnrat' theorem

(h : ∀ n : ℕ, f n = g n) : f = g

Full source

/-- If monoid with zero homs `f` and `g` from `ℚ≥0` agree on the naturals then they are equal. -/
lemma ext_nnrat' (h : ∀ n : ℕ, f n = g n) : f = g :=
  (DFunLike.ext f g) fun r => by
    rw [← r.num_div_den, div_eq_mul_inv, map_mul, map_mul, h, eq_on_inv₀ f g]
    apply h

Uniqueness of Monoid with Zero Homomorphisms from Nonnegative Rationals via Natural Numbers

Informal description

If two monoid with zero homomorphisms $f$ and $g$ from the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ to a monoid with zero $M_0$ agree on all natural numbers, then they are equal, i.e., $f = g$.

MonoidWithZeroHomClass.ext_nnrat theorem

 {f g : ℚ≥0 →*₀ M₀} (h : f.comp (Nat.castRingHom ℚ≥0 : ℕ →*₀ ℚ≥0) = g.comp (Nat.castRingHom ℚ≥0)) : f = g

Full source

/-- If monoid with zero homs `f` and `g` from `ℚ≥0` agree on the naturals then they are equal.

See note [partially-applied ext lemmas] for why `comp` is used here. -/
@[ext]
lemma ext_nnrat {f g : ℚ≥0ℚ≥0 →*₀ M₀}
    (h : f.comp (Nat.castRingHom ℚ≥0 : ℕℕ →*₀ ℚ≥0) = g.comp (Nat.castRingHom ℚ≥0)) : f = g :=
  ext_nnrat' <| DFunLike.congr_fun h

Uniqueness of Monoid Homomorphisms from Nonnegative Rationals via Natural Number Composition

Informal description

Let $f, g : \mathbb{Q}_{\geq 0} \to M_0$ be monoid with zero homomorphisms. If the compositions of $f$ and $g$ with the canonical ring homomorphism $\mathbb{N} \to \mathbb{Q}_{\geq 0}$ are equal, then $f = g$.

MonoidWithZeroHomClass.ext_nnrat_on_pnat theorem

(same_on_pnat : ∀ n : ℕ, 0 < n → f n = g n) : f = g

Full source

/-- If monoid with zero homs `f` and `g` from `ℚ≥0` agree on the positive naturals then they are
equal. -/
lemma ext_nnrat_on_pnat (same_on_pnat : ∀ n : ℕ, 0 < n → f n = g n) : f = g :=
  ext_nnrat' <| DFunLike.congr_fun <| ext_nat''
    ((f : ℚ≥0ℚ≥0 →*₀ M₀).comp (Nat.castRingHom ℚ≥0 : ℕℕ →*₀ ℚ≥0))
    ((g : ℚ≥0ℚ≥0 →*₀ M₀).comp (Nat.castRingHom ℚ≥0 : ℕℕ →*₀ ℚ≥0)) (by simpa)

Uniqueness of Monoid with Zero Homomorphisms from Nonnegative Rationals via Positive Natural Numbers

Informal description

Let $f$ and $g$ be monoid with zero homomorphisms from the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ to a monoid with zero $M_0$. If $f$ and $g$ agree on all positive natural numbers (i.e., $f(n) = g(n)$ for all $n \in \mathbb{N}$ with $n > 0$), then $f = g$.

MonoidWithZeroHomClass.ext_rat' theorem

(h : ∀ m : ℤ, f m = g m) : f = g

Full source

/-- If monoid with zero homs `f` and `g` from `ℚ` agree on the integers then they are equal. -/
theorem ext_rat' (h : ∀ m : ℤ, f m = g m) : f = g :=
  (DFunLike.ext f g) fun r => by
    rw [← r.num_div_den, div_eq_mul_inv, map_mul, map_mul, h, ← Int.cast_natCast,
      eq_on_inv₀ f g]
    apply h

Uniqueness of Monoid Homomorphisms from Rationals via Integer Agreement

Informal description

Let $f$ and $g$ be monoid with zero homomorphisms from $\mathbb{Q}$ to a division ring. If $f$ and $g$ agree on all integer inputs (i.e., $f(m) = g(m)$ for all $m \in \mathbb{Z}$), then $f = g$.

MonoidWithZeroHomClass.ext_rat theorem

{f g : ℚ →*₀ M₀} (h : f.comp (Int.castRingHom ℚ : ℤ →*₀ ℚ) = g.comp (Int.castRingHom ℚ)) : f = g

Full source

/-- If monoid with zero homs `f` and `g` from `ℚ` agree on the integers then they are equal.

See note [partially-applied ext lemmas] for why `comp` is used here. -/
@[ext]
theorem ext_rat {f g : ℚℚ →*₀ M₀}
    (h : f.comp (Int.castRingHom ℚ : ℤℤ →*₀ ℚ) = g.comp (Int.castRingHom ℚ)) : f = g :=
  ext_rat' <| DFunLike.congr_fun h

Uniqueness of Monoid Homomorphisms from Rationals via Integer Composition

Informal description

Let $f$ and $g$ be monoid with zero homomorphisms from $\mathbb{Q}$ to $M₀$. If the compositions of $f$ and $g$ with the canonical ring homomorphism from $\mathbb{Z}$ to $\mathbb{Q}$ are equal, then $f = g$.

MonoidWithZeroHomClass.ext_rat_on_pnat theorem

(same_on_neg_one : f (-1) = g (-1)) (same_on_pnat : ∀ n : ℕ, 0 < n → f n = g n) : f = g

Full source

/-- If monoid with zero homs `f` and `g` from `ℚ` agree on the positive naturals and `-1` then
they are equal. -/
theorem ext_rat_on_pnat (same_on_neg_one : f (-1) = g (-1))
    (same_on_pnat : ∀ n : ℕ, 0 < n → f n = g n) : f = g :=
  ext_rat' <|
    DFunLike.congr_fun <|
      show
        (f : ℚℚ →*₀ M₀).comp (Int.castRingHom ℚ : ℤℤ →*₀ ℚ) =
          (g : ℚℚ →*₀ M₀).comp (Int.castRingHom ℚ : ℤℤ →*₀ ℚ)
        from ext_int' (by simpa) (by simpa)

Uniqueness of Monoid Homomorphisms from Rationals via Agreement on $-1$ and Positive Naturals

Informal description

Let $f$ and $g$ be monoid with zero homomorphisms from $\mathbb{Q}$ to a division ring. If $f$ and $g$ agree on $-1$ (i.e., $f(-1) = g(-1)$) and on all positive natural numbers (i.e., $f(n) = g(n)$ for all $n \in \mathbb{N}$ with $0 < n$), then $f = g$.

RingHom.ext_rat theorem

{R : Type*} [Semiring R] [FunLike F ℚ R] [RingHomClass F ℚ R] (f g : F) : f = g

Full source

/-- Any two ring homomorphisms from `ℚ` to a semiring are equal. If the codomain is a division ring,
then this lemma follows from `eq_ratCast`. -/
theorem RingHom.ext_rat {R : Type*} [Semiring R] [FunLike F ℚ R] [RingHomClass F ℚ R] (f g : F) :
    f = g :=
  MonoidWithZeroHomClass.ext_rat' <|
    RingHom.congr_fun <|
      ((f : ℚℚ →+* R).comp (Int.castRingHom ℚ)).ext_int ((g : ℚℚ →+* R).comp (Int.castRingHom ℚ))

Uniqueness of Ring Homomorphisms from Rationals to a Semiring

Informal description

Let $R$ be a semiring and let $F$ be a type with a function-like structure from $\mathbb{Q}$ to $R$ that is also a ring homomorphism class. Then any two ring homomorphisms $f, g \colon \mathbb{Q} \to R$ in $F$ are equal.

NNRat.subsingleton_ringHom instance

{R : Type*} [Semiring R] : Subsingleton (ℚ≥0 →+* R)

Full source

instance NNRat.subsingleton_ringHom {R : Type*} [Semiring R] : Subsingleton (ℚ≥0ℚ≥0 →+* R) where
  allEq f g := MonoidWithZeroHomClass.ext_nnrat' <| by simp

Uniqueness of Ring Homomorphisms from Nonnegative Rationals

Informal description

For any semiring $R$, there is at most one ring homomorphism from the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ to $R$.

Rat.subsingleton_ringHom instance

{R : Type*} [Semiring R] : Subsingleton (ℚ →+* R)

Full source

instance Rat.subsingleton_ringHom {R : Type*} [Semiring R] : Subsingleton (ℚℚ →+* R) :=
  ⟨RingHom.ext_rat⟩

Uniqueness of Ring Homomorphisms from Rationals to a Semiring

Informal description

For any semiring $R$, there is at most one ring homomorphism from the rational numbers $\mathbb{Q}$ to $R$.

Mathlib.Data.Rat.Cast.Defs

Summary

Tags