Rationals approximate any field

We want to do power series computations over ℚ, where these approximate ℂ via field structure. This works because our spray series functions uses only field operations on scalars.

instance Rat.instApproxField {𝕜 : Type} [Field 𝕜] : Approx ℚ 𝕜

Equations

• Rat.instApproxField = { approx := fun (x : ℚ) (x' : 𝕜) => ↑x = x' }

theorem Rat.approx {𝕜 : Type} [Field 𝕜] {x : ℚ} {x' : 𝕜} : Approx.approx x x' ↔ ↑x = x'

instance instApproxZeroRat {𝕜 : Type} [Field 𝕜] : ApproxZero ℚ 𝕜

instance instApproxZeroIffRat {𝕜 : Type} [Field 𝕜] : ApproxZeroIff ℚ 𝕜

instance instApproxOneRat {𝕜 : Type} [Field 𝕜] : ApproxOne ℚ 𝕜

instance instApproxNegRat {𝕜 : Type} [Field 𝕜] : ApproxNeg ℚ 𝕜

instance instApproxAddRat {𝕜 : Type} [Field 𝕜] [CharZero 𝕜] : ApproxAdd ℚ 𝕜

instance instApproxSubRat {𝕜 : Type} [Field 𝕜] [CharZero 𝕜] : ApproxSub ℚ 𝕜

instance instApproxMulRat {𝕜 : Type} [Field 𝕜] [CharZero 𝕜] : ApproxMul ℚ 𝕜

instance instApproxInvRat {𝕜 : Type} [Field 𝕜] [CharZero 𝕜] : ApproxInv ℚ 𝕜

instance instApproxDivRat {𝕜 : Type} [Field 𝕜] [CharZero 𝕜] : ApproxDiv ℚ 𝕜

instance instApproxSMulRat {𝕜 : Type} [Field 𝕜] : ApproxSMul ℚ 𝕜 𝕜 𝕜

instance instApproxNatCastRat {𝕜 : Type} [Field 𝕜] : ApproxNatCast ℚ 𝕜

instance instApproxIntCastRat {𝕜 : Type} [Field 𝕜] : ApproxIntCast ℚ 𝕜

instance instApproxRatCastRat {𝕜 : Type} [Field 𝕜] : ApproxRatCast ℚ 𝕜

instance instApproxDiv2Rat {𝕜 : Type} [Field 𝕜] [CharZero 𝕜] : ApproxDiv2 ℚ 𝕜