Casts for Rational Numbers #
Summary #
We define the canonical injection from ℚ into an arbitrary division ring and prove various casting lemmas showing the well-behavedness of this injection.
Notations #
/.
is infix notation forRat.divInt
.
Tags #
rat, rationals, field, ℚ, numerator, denominator, num, denom, cast, coercion, casting
@[simp]
theorem
NNRat.cast_ofNat
{α : Type u_3}
[DivisionSemiring α]
(n : ℕ)
[n.AtLeastTwo]
:
↑(OfNat.ofNat n) = OfNat.ofNat n
theorem
NNRat.cast_divNat_of_ne_zero
{α : Type u_3}
[DivisionSemiring α]
(a : ℕ)
{b : ℕ}
(hb : ↑b ≠ 0)
:
↑(NNRat.divNat a b) = ↑a / ↑b
@[deprecated Rat.cast_intCast]
Alias of Rat.cast_intCast
.
@[deprecated Rat.cast_natCast]
Alias of Rat.cast_natCast
.
@[simp]
theorem
Rat.cast_ofNat
{α : Type u_3}
[DivisionRing α]
(n : ℕ)
[n.AtLeastTwo]
:
↑(OfNat.ofNat n) = OfNat.ofNat n
theorem
Rat.cast_divInt_of_ne_zero
{α : Type u_3}
[DivisionRing α]
(a : ℤ)
{b : ℤ}
(b0 : ↑b ≠ 0)
:
↑(Rat.divInt a b) = ↑a / ↑b
@[simp]
theorem
map_nnratCast
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[FunLike F α β]
[DivisionSemiring α]
[DivisionSemiring β]
[RingHomClass F α β]
(f : F)
(q : ℚ≥0)
:
f ↑q = ↑q
@[simp]
theorem
eq_nnratCast
{F : Type u_1}
{α : Type u_3}
[DivisionSemiring α]
[FunLike F ℚ≥0 α]
[RingHomClass F ℚ≥0 α]
(f : F)
(q : ℚ≥0)
:
f q = ↑q
@[simp]
theorem
map_ratCast
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[FunLike F α β]
[DivisionRing α]
[DivisionRing β]
[RingHomClass F α β]
(f : F)
(q : ℚ)
:
f ↑q = ↑q
@[simp]
theorem
eq_ratCast
{F : Type u_1}
{α : Type u_3}
[DivisionRing α]
[FunLike F ℚ α]
[RingHomClass F ℚ α]
(f : F)
(q : ℚ)
:
f q = ↑q
theorem
MonoidWithZeroHom.ext_rat'
{F : Type u_1}
{M₀ : Type u_5}
[MonoidWithZero M₀]
[FunLike F ℚ M₀]
[MonoidWithZeroHomClass F ℚ M₀]
{f : F}
{g : F}
(h : ∀ (m : ℤ), f ↑m = g ↑m)
:
f = g
If f
and g
agree on the integers then they are equal φ
.
theorem
MonoidWithZeroHom.ext_rat
{M₀ : Type u_5}
[MonoidWithZero M₀]
{f : ℚ →*₀ M₀}
{g : ℚ →*₀ M₀}
(h : f.comp ↑(Int.castRingHom ℚ) = g.comp ↑(Int.castRingHom ℚ))
:
f = g
If f
and g
agree on the integers then they are equal φ
.
See note [partially-applied ext lemmas] for why comp
is used here.
theorem
MonoidWithZeroHom.ext_rat_on_pnat
{F : Type u_1}
{M₀ : Type u_5}
[MonoidWithZero M₀]
[FunLike F ℚ M₀]
[MonoidWithZeroHomClass F ℚ M₀]
{f : F}
{g : F}
(same_on_neg_one : f (-1) = g (-1))
(same_on_pnat : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n)
:
f = g
Positive integer values of a morphism φ
and its value on -1
completely determine φ
.
theorem
RingHom.ext_rat
{F : Type u_1}
{R : Type u_5}
[Semiring R]
[FunLike F ℚ R]
[RingHomClass F ℚ R]
(f : F)
(g : F)
:
f = g
Any two ring homomorphisms from ℚ
to a semiring are equal. If the codomain is a division ring,
then this lemma follows from eq_ratCast
.
Equations
- ⋯ = ⋯
Scalar multiplication #
@[instance 100]
Equations
- NNRat.instDistribSMul = DistribSMul.mk ⋯
Equations
- ⋯ = ⋯
@[instance 100]
Equations
- Rat.instDistribSMul = DistribSMul.mk ⋯
Equations
- ⋯ = ⋯