1.10. Cast lemmas🔗

instance instNNRatCast : NNRatCast ℚ[i] where nnratCast q := ofRational q instance instRatCast : RatCast ℚ[i] where ratCast q := ofRational q @[simp, norm_cast] lemma ofRational_ofNat (n : ℕ) [n.AtLeastTwo] : ofRational (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl @[simp, norm_cast] lemma ofRational_natCast (n : ℕ) : ofRational n = n := rfl @[simp, norm_cast] lemma ofRational_intCast (n : ℤ) : ofRational n = n := rfl @[simp, norm_cast] lemma ofRational_nnratCast (q : ℚ≥0) : ofRational q = q := rfl @[simp] lemma ofRational_ratCast (q : ℚ) : ofRational q = q := rfl @[simp] lemma re_ofNat (n : ℕ) [n.AtLeastTwo] : (no_index (OfNat.ofNat n) : ℚ[i]).re = OfNat.ofNat n := rfl @[simp] lemma im_ofNat (n : ℕ) [n.AtLeastTwo] : (no_index (OfNat.ofNat n) : ℚ[i]).im = 0 := rfl @[simp, norm_cast] lemma natCast_re (n : ℕ) : (n : ℚ[i]).re = n := rfl @[simp, norm_cast] lemma natCast_im (n : ℕ) : (n : ℚ[i]).im = 0 := rfl @[simp, norm_cast] lemma intCast_re (n : ℤ) : (n : ℚ[i]).re = n := rfl @[simp, norm_cast] lemma intCast_im (n : ℤ) : (n : ℚ[i]).im = 0 := rfl @[simp, norm_cast] lemma re_nnratCast (q : ℚ≥0) : (q : ℚ[i]).re = q := rfl @[simp, norm_cast] lemma im_nnratCast (q : ℚ≥0) : (q : ℚ[i]).im = 0 := rfl @[simp, norm_cast] lemma ratCast_re (q : ℚ) : (q : ℚ[i]).re = q := rfl @[simp, norm_cast] lemma ratCast_im (q : ℚ) : (q : ℚ[i]).im = 0 := rfl lemma ofRational_nsmul (n : ℕ) (r : ℚ) : ↑(n • r) = n • (r : ℚ[i]) := byn:ℕr:ℚ⊢ ↑(n • r) = n • ↑r simpn:ℕr:ℚ⊢ ↑(↑n * r) = ↑n * ↑r refine ext_iff.mpr ?_n:ℕr:ℚ⊢ (↑(↑n * r)).re = (↑n * ↑r).re ∧ (↑(↑n * r)).im = (↑n * ↑r).im constructorleftn:ℕr:ℚ⊢ (↑(↑n * r)).re = (↑n * ↑r).rerightn:ℕr:ℚ⊢ (↑(↑n * r)).im = (↑n * ↑r).im ·leftn:ℕr:ℚ⊢ (↑(↑n * r)).re = (↑n * ↑r).re dsimpleftn:ℕr:ℚ⊢ ↑n * r = ↑n * r - 0 * 0 ringAll goals completed! 🐙 ·rightn:ℕr:ℚ⊢ (↑(↑n * r)).im = (↑n * ↑r).im simpAll goals completed! 🐙 lemma ofRational_zsmul (n : ℤ) (r : ℚ) : ↑(n • r) = n • (r : ℚ[i]) := byn:ℤr:ℚ⊢ ↑(n • r) = n • ↑r simpn:ℤr:ℚ⊢ ↑(↑n * r) = ↑n * ↑r refine ext_iff.mpr ?_n:ℤr:ℚ⊢ (↑(↑n * r)).re = (↑n * ↑r).re ∧ (↑(↑n * r)).im = (↑n * ↑r).im constructorleftn:ℤr:ℚ⊢ (↑(↑n * r)).re = (↑n * ↑r).rerightn:ℤr:ℚ⊢ (↑(↑n * r)).im = (↑n * ↑r).im ·leftn:ℤr:ℚ⊢ (↑(↑n * r)).re = (↑n * ↑r).re dsimpleftn:ℤr:ℚ⊢ ↑n * r = ↑n * r - 0 * 0 ringAll goals completed! 🐙 ·rightn:ℤr:ℚ⊢ (↑(↑n * r)).im = (↑n * ↑r).im simpAll goals completed! 🐙