Documentation

Mathlib.Data.Rat.Cast.Defs

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.

Tags #

rat, rationals, field, โ„š, numerator, denominator, num, denom, cast, coercion, casting

source
๐Ÿ“ coverage
@[simp]
theorem NNRat.cast_natCast {ฮฑ : Type u_3} [DivisionSemiring ฮฑ] (n : โ„•) :
โ†‘โ†‘n = โ†‘n
source
๐Ÿ“ coverage
@[simp]
theorem NNRat.cast_ofNat {ฮฑ : Type u_3} [DivisionSemiring ฮฑ] (n : โ„•) [n.AtLeastTwo] :
โ†‘(OfNat.ofNat n) = OfNat.ofNat n
source
๐Ÿ“ coverage
@[simp]
theorem NNRat.cast_zero {ฮฑ : Type u_3} [DivisionSemiring ฮฑ] :
โ†‘0 = 0
source
๐Ÿ“ coverage
@[simp]
theorem NNRat.cast_one {ฮฑ : Type u_3} [DivisionSemiring ฮฑ] :
โ†‘1 = 1
source
๐Ÿ“ coverage
theorem NNRat.cast_commute {ฮฑ : Type u_3} [DivisionSemiring ฮฑ] (q : โ„šโ‰ฅ0) (a : ฮฑ) :
Commute (โ†‘q) a
source
๐Ÿ“ coverage
theorem NNRat.commute_cast {ฮฑ : Type u_3} [DivisionSemiring ฮฑ] (a : ฮฑ) (q : โ„šโ‰ฅ0) :
Commute a โ†‘q
source
๐Ÿ“ coverage
theorem NNRat.cast_comm {ฮฑ : Type u_3} [DivisionSemiring ฮฑ] (q : โ„šโ‰ฅ0) (a : ฮฑ) :
โ†‘q * a = a * โ†‘q
source
๐Ÿ“ coverage
theorem NNRat.cast_divNat_of_ne_zero {ฮฑ : Type u_3} [DivisionSemiring ฮฑ] (a : โ„•) {b : โ„•} (hb : โ†‘b โ‰  0) :
โ†‘(divNat a b) = โ†‘a / โ†‘b
source
๐Ÿ“ coverage
theorem NNRat.cast_add_of_ne_zero {ฮฑ : Type u_3} [DivisionSemiring ฮฑ] {q r : โ„šโ‰ฅ0} (hq : โ†‘q.den โ‰  0) (hr : โ†‘r.den โ‰  0) :
โ†‘(q + r) = โ†‘q + โ†‘r
source
๐Ÿ“ coverage
theorem NNRat.cast_mul_of_ne_zero {ฮฑ : Type u_3} [DivisionSemiring ฮฑ] {q r : โ„šโ‰ฅ0} (hq : โ†‘q.den โ‰  0) (hr : โ†‘r.den โ‰  0) :
โ†‘(q * r) = โ†‘q * โ†‘r
source
๐Ÿ“ coverage
theorem NNRat.cast_inv_of_ne_zero {ฮฑ : Type u_3} [DivisionSemiring ฮฑ] {q : โ„šโ‰ฅ0} (hq : โ†‘q.num โ‰  0) :
โ†‘qโปยน = (โ†‘q)โปยน
source
๐Ÿ“ coverage
theorem NNRat.cast_div_of_ne_zero {ฮฑ : Type u_3} [DivisionSemiring ฮฑ] {q r : โ„šโ‰ฅ0} (hq : โ†‘q.den โ‰  0) (hr : โ†‘r.num โ‰  0) :
โ†‘(q / r) = โ†‘q / โ†‘r
source
๐Ÿ“ coverage
@[simp]
theorem Rat.cast_intCast {ฮฑ : Type u_3} [DivisionRing ฮฑ] (n : โ„ค) :
โ†‘โ†‘n = โ†‘n
source
๐Ÿ“ coverage
@[simp]
theorem Rat.cast_natCast {ฮฑ : Type u_3} [DivisionRing ฮฑ] (n : โ„•) :
โ†‘โ†‘n = โ†‘n
source
๐Ÿ“ coverage
@[simp]
theorem Rat.cast_ofNat {ฮฑ : Type u_3} [DivisionRing ฮฑ] (n : โ„•) [n.AtLeastTwo] :
โ†‘(OfNat.ofNat n) = OfNat.ofNat n
source
๐Ÿ“ coverage
@[simp]
theorem Rat.cast_zero {ฮฑ : Type u_3} [DivisionRing ฮฑ] :
โ†‘0 = 0
source
๐Ÿ“ coverage
@[simp]
theorem Rat.cast_one {ฮฑ : Type u_3} [DivisionRing ฮฑ] :
โ†‘1 = 1
source
๐Ÿ“ coverage
theorem Rat.cast_commute {ฮฑ : Type u_3} [DivisionRing ฮฑ] (r : โ„š) (a : ฮฑ) :
Commute (โ†‘r) a
source
๐Ÿ“ coverage
theorem Rat.cast_comm {ฮฑ : Type u_3} [DivisionRing ฮฑ] (r : โ„š) (a : ฮฑ) :
โ†‘r * a = a * โ†‘r
source
๐Ÿ“ coverage
theorem Rat.commute_cast {ฮฑ : Type u_3} [DivisionRing ฮฑ] (a : ฮฑ) (r : โ„š) :
Commute a โ†‘r
source
๐Ÿ“ coverage
theorem Rat.cast_divInt_of_ne_zero {ฮฑ : Type u_3} [DivisionRing ฮฑ] (a : โ„ค) {b : โ„ค} (b0 : โ†‘b โ‰  0) :
โ†‘(divInt a b) = โ†‘a / โ†‘b
source
๐Ÿ“ coverage
theorem Rat.cast_mkRat_of_ne_zero {ฮฑ : Type u_3} [DivisionRing ฮฑ] (a : โ„ค) {b : โ„•} (hb : โ†‘b โ‰  0) :
โ†‘(mkRat a b) = โ†‘a / โ†‘b
source
๐Ÿ“ coverage
theorem Rat.cast_add_of_ne_zero {ฮฑ : Type u_3} [DivisionRing ฮฑ] {q r : โ„š} (hq : โ†‘q.den โ‰  0) (hr : โ†‘r.den โ‰  0) :
โ†‘(q + r) = โ†‘q + โ†‘r
source
๐Ÿ“ coverage
@[simp]
theorem Rat.cast_neg {ฮฑ : Type u_3} [DivisionRing ฮฑ] (q : โ„š) :
โ†‘(-q) = -โ†‘q
source
๐Ÿ“ coverage
theorem Rat.cast_sub_of_ne_zero {ฮฑ : Type u_3} [DivisionRing ฮฑ] {p q : โ„š} (hp : โ†‘p.den โ‰  0) (hq : โ†‘q.den โ‰  0) :
โ†‘(p - q) = โ†‘p - โ†‘q
source
๐Ÿ“ coverage
theorem Rat.cast_mul_of_ne_zero {ฮฑ : Type u_3} [DivisionRing ฮฑ] {p q : โ„š} (hp : โ†‘p.den โ‰  0) (hq : โ†‘q.den โ‰  0) :
โ†‘(p * q) = โ†‘p * โ†‘q
source
๐Ÿ“ coverage
theorem Rat.cast_inv_of_ne_zero {ฮฑ : Type u_3} [DivisionRing ฮฑ] {q : โ„š} (hq : โ†‘q.num โ‰  0) :
โ†‘qโปยน = (โ†‘q)โปยน
source
๐Ÿ“ coverage
theorem Rat.cast_div_of_ne_zero {ฮฑ : Type u_3} [DivisionRing ฮฑ] {p q : โ„š} (hp : โ†‘p.den โ‰  0) (hq : โ†‘q.num โ‰  0) :
โ†‘(p / q) = โ†‘p / โ†‘q
source
๐Ÿ“ coverage
@[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
source
๐Ÿ“ coverage
@[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
source
๐Ÿ“ coverage
@[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
source
๐Ÿ“ coverage
@[simp]
theorem eq_ratCast {F : Type u_1} {ฮฑ : Type u_3} [DivisionRing ฮฑ] [FunLike F โ„š ฮฑ] [RingHomClass F โ„š ฮฑ] (f : F) (q : โ„š) :
f q = โ†‘q
source
theorem MonoidWithZeroHomClass.ext_nnrat' {F : Type u_1} {Mโ‚€ : Type u_5} [MonoidWithZero Mโ‚€] [FunLike F โ„šโ‰ฅ0 Mโ‚€] [MonoidWithZeroHomClass F โ„šโ‰ฅ0 Mโ‚€] {f g : F} (h : โˆ€ (n : โ„•), f โ†‘n = g โ†‘n) :
f = g

If monoid with zero homs f and g from โ„šโ‰ฅ0 agree on the naturals then they are equal.

source
theorem MonoidWithZeroHomClass.ext_nnrat {Mโ‚€ : Type u_5} [MonoidWithZero Mโ‚€] {f g : โ„šโ‰ฅ0 โ†’*โ‚€ Mโ‚€} (h : f.comp โ†‘(Nat.castRingHom โ„šโ‰ฅ0) = g.comp โ†‘(Nat.castRingHom โ„šโ‰ฅ0)) :
f = g

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.

source
๐Ÿ“ coverage
theorem MonoidWithZeroHomClass.ext_nnrat_iff {Mโ‚€ : Type u_5} [MonoidWithZero Mโ‚€] {f g : โ„šโ‰ฅ0 โ†’*โ‚€ Mโ‚€} :
f = g โ†” f.comp โ†‘(Nat.castRingHom โ„šโ‰ฅ0) = g.comp โ†‘(Nat.castRingHom โ„šโ‰ฅ0)
source
theorem MonoidWithZeroHomClass.ext_nnrat_on_pnat {F : Type u_1} {Mโ‚€ : Type u_5} [MonoidWithZero Mโ‚€] [FunLike F โ„šโ‰ฅ0 Mโ‚€] [MonoidWithZeroHomClass F โ„šโ‰ฅ0 Mโ‚€] {f g : F} (same_on_pnat : โˆ€ (n : โ„•), 0 < n โ†’ f โ†‘n = g โ†‘n) :
f = g

If monoid with zero homs f and g from โ„šโ‰ฅ0 agree on the positive naturals then they are equal.

source
theorem MonoidWithZeroHomClass.ext_rat' {F : Type u_1} {Mโ‚€ : Type u_5} [MonoidWithZero Mโ‚€] [FunLike F โ„š Mโ‚€] [MonoidWithZeroHomClass F โ„š Mโ‚€] {f g : F} (h : โˆ€ (m : โ„ค), f โ†‘m = g โ†‘m) :
f = g

If monoid with zero homs f and g from โ„š agree on the integers then they are equal.

source
theorem MonoidWithZeroHomClass.ext_rat {Mโ‚€ : Type u_5} [MonoidWithZero Mโ‚€] {f g : โ„š โ†’*โ‚€ Mโ‚€} (h : f.comp โ†‘(Int.castRingHom โ„š) = g.comp โ†‘(Int.castRingHom โ„š)) :
f = g

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.

source
๐Ÿ“ coverage
theorem MonoidWithZeroHomClass.ext_rat_iff {Mโ‚€ : Type u_5} [MonoidWithZero Mโ‚€] {f g : โ„š โ†’*โ‚€ Mโ‚€} :
f = g โ†” f.comp โ†‘(Int.castRingHom โ„š) = g.comp โ†‘(Int.castRingHom โ„š)
source
theorem MonoidWithZeroHomClass.ext_rat_on_pnat {F : Type u_1} {Mโ‚€ : Type u_5} [MonoidWithZero Mโ‚€] [FunLike F โ„š Mโ‚€] [MonoidWithZeroHomClass F โ„š Mโ‚€] {f g : F} (same_on_neg_one : f (-1) = g (-1)) (same_on_pnat : โˆ€ (n : โ„•), 0 < n โ†’ f โ†‘n = g โ†‘n) :
f = g

If monoid with zero homs f and g from โ„š agree on the positive naturals and -1 then they are equal.

source
theorem RingHom.ext_rat {F : Type u_1} {R : Type u_5} [Semiring R] [FunLike F โ„š R] [RingHomClass F โ„š R] (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.

source
๐Ÿ“ coverage
instance NNRat.subsingleton_ringHom {R : Type u_5} [Semiring R] :
Subsingleton (โ„šโ‰ฅ0 โ†’+* R)
source
๐Ÿ“ coverage
instance Rat.subsingleton_ringHom {R : Type u_5} [Semiring R] :
Subsingleton (โ„š โ†’+* R)