feat(algebra/field/basic): nnrat.cast

src/algebra/field/basic.lean

@@ -17,14 +17,15 @@ import algebra.ring.inj_surj
 -/
 
 open function order_dual set
+open_locale nnrat
 
 set_option old_structure_cmd true
 
 universe u
 variables {α β K : Type*}
 
 section division_semiring
-variables [division_semiring α] {a b c : α}
+variables [division_semiring α] {a b c d : α}
 
 lemma add_div (a b c : α) : (a + b) / c = a / c + b / c := by simp_rw [div_eq_mul_inv, add_mul]
 
@@ -50,6 +51,10 @@ by rw [add_div, mul_div_cancel _ hc]
 @[field_simps] lemma div_add' (a b c : α) (hc : c ≠ 0) : a / c + b = (a + b * c) / c :=
 by rwa [add_comm, add_div', add_comm]
 
+lemma commute.div_add_div (hbc : commute b c) (hbd : commute b d) (hb : b ≠ 0) (hd : d ≠ 0) :
+  a / b + c / d = (a * d + b * c) / (b * d) :=
+by rw [add_div, mul_div_mul_right _ b hd, hbc.eq, hbd.eq, mul_div_mul_right c d hb]
+
 end division_semiring
 
 section division_monoid
@@ -138,7 +143,7 @@ variables [semifield α] {a b c d : α}
 
 lemma div_add_div (a : α) (c : α) (hb : b ≠ 0) (hd : d ≠ 0) :
   (a / b) + (c / d) = ((a * d) + (b * c)) / (b * d) :=
-by rw [← mul_div_mul_right _ b hd, ← mul_div_mul_left c d hb, div_add_div_same]
+(commute.all b _).div_add_div (commute.all _ _) hb hd
 
 lemma one_div_add_one_div (ha : a ≠ 0) (hb : b ≠ 0) : 1 / a + 1 / b = (a + b) / (a * b) :=
 by rw [div_add_div _ _ ha hb, one_mul, mul_one, add_comm]
@@ -206,99 +211,111 @@ end noncomputable_defs
 /-- Pullback a `division_semiring` along an injective function. -/
 @[reducible] -- See note [reducible non-instances]
 protected def function.injective.division_semiring [division_semiring β] [has_zero α] [has_mul α]
-  [has_add α] [has_one α] [has_inv α] [has_div α] [has_smul ℕ α] [has_pow α ℕ] [has_pow α ℤ]
-  [has_nat_cast α]
+  [has_add α] [has_one α] [has_inv α] [has_div α] [has_smul ℕ α] [has_smul ℚ≥0 α] [has_pow α ℕ]
+  [has_pow α ℤ] [has_nat_cast α] [has_nnrat_cast α]
   (f : α → β) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
   (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
   (inv : ∀ x, f (x⁻¹) = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
-  (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x)
+  (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (nnqsmul : ∀ x (q : ℚ≥0), f (q • x) = q • f x)
   (npow : ∀ x (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ x (n : ℤ), f (x ^ n) = f x ^ n)
-  (nat_cast : ∀ n : ℕ, f n = n) :
+  (nat_cast : ∀ n : ℕ, f n = n) (nnrat_cast : ∀ q : ℚ≥0, f q = q) :
   division_semiring α :=
-{ .. hf.group_with_zero f zero one mul inv div npow zpow,
+{ nnrat_cast := coe,
+  nnrat_cast_eq := λ q, hf $ by erw [nnrat_cast, nnrat.cast_def, div, nat_cast, nat_cast],
+  nnqsmul := (•),
+  nnqsmul_eq_mul := λ a x, hf $ by erw [nnqsmul, mul, nnrat_cast, nnrat.smul_def],
+  .. hf.group_with_zero f zero one mul inv div npow zpow,
   .. hf.semiring f zero one add mul nsmul npow nat_cast }
 
 /-- Pullback a `division_ring` along an injective function.
 See note [reducible non-instances]. -/
 @[reducible]
 protected def function.injective.division_ring [division_ring K] {K'}
   [has_zero K'] [has_one K'] [has_add K'] [has_mul K'] [has_neg K'] [has_sub K'] [has_inv K']
-  [has_div K'] [has_smul ℕ K'] [has_smul ℤ K'] [has_smul ℚ K'] [has_pow K' ℕ] [has_pow K' ℤ]
-  [has_nat_cast K'] [has_int_cast K'] [has_rat_cast K']
+  [has_div K'] [has_smul ℕ K'] [has_smul ℤ K'] [has_smul ℚ≥0 K'] [has_smul ℚ K'] [has_pow K' ℕ]
+  [has_pow K' ℤ] [has_nat_cast K'] [has_int_cast K'] [has_nnrat_cast K'] [has_rat_cast K']
   (f : K' → K) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
   (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
   (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
   (inv : ∀ x, f (x⁻¹) = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
   (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ x (n : ℤ), f (n • x) = n • f x)
-  (qsmul : ∀ x (n : ℚ), f (n • x) = n • f x)
+  (nnqsmul : ∀ x (q : ℚ≥0), f (q • x) = q • f x) (qsmul : ∀ x (q : ℚ), f (q • x) = q • f x)
   (npow : ∀ x (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ x (n : ℤ), f (x ^ n) = f x ^ n)
-  (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) (rat_cast : ∀ n : ℚ, f n = n) :
+  (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) (nnrat_cast : ∀ q : ℚ≥0, f q = q)
+  (rat_cast : ∀ q : ℚ, f q = q) :
   division_ring K' :=
 { rat_cast := coe,
   rat_cast_mk := λ a b h1 h2, hf (by erw [rat_cast, mul, inv, int_cast, nat_cast];
                                      exact division_ring.rat_cast_mk a b h1 h2),
   qsmul := (•),
   qsmul_eq_mul' := λ a x, hf (by erw [qsmul, mul, rat.smul_def, rat_cast]),
-  .. hf.group_with_zero f zero one mul inv div npow zpow,
+  .. hf.division_semiring f zero one add mul inv div nsmul nnqsmul npow zpow nat_cast nnrat_cast,
   .. hf.ring f zero one add mul neg sub nsmul zsmul npow nat_cast int_cast }
 
 /-- Pullback a `field` along an injective function. -/
 @[reducible] -- See note [reducible non-instances]
 protected def function.injective.semifield [semifield β] [has_zero α] [has_mul α] [has_add α]
-  [has_one α] [has_inv α] [has_div α] [has_smul ℕ α] [has_pow α ℕ] [has_pow α ℤ]
-  [has_nat_cast α]
+  [has_one α] [has_inv α] [has_div α] [has_smul ℕ α] [has_smul ℚ≥0 α] [has_pow α ℕ] [has_pow α ℤ]
+  [has_nat_cast α] [has_nnrat_cast α]
   (f : α → β) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
   (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
   (inv : ∀ x, f (x⁻¹) = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
-  (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x)
+  (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (nnqsmul : ∀ x (q : ℚ≥0), f (q • x) = q • f x)
   (npow : ∀ x (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ x (n : ℤ), f (x ^ n) = f x ^ n)
-  (nat_cast : ∀ n : ℕ, f n = n) :
+  (nat_cast : ∀ n : ℕ, f n = n) (nnrat_cast : ∀ q : ℚ≥0, f q = q) :
   semifield α :=
-{ .. hf.comm_group_with_zero f zero one mul inv div npow zpow,
+{ .. hf.division_semiring f zero one add mul inv div nsmul nnqsmul npow zpow nat_cast nnrat_cast,
   .. hf.comm_semiring f zero one add mul nsmul npow nat_cast }
 
 /-- Pullback a `field` along an injective function.
 See note [reducible non-instances]. -/
 @[reducible]
 protected def function.injective.field [field K] {K'}
   [has_zero K'] [has_mul K'] [has_add K'] [has_neg K'] [has_sub K'] [has_one K'] [has_inv K']
-  [has_div K'] [has_smul ℕ K'] [has_smul ℤ K'] [has_smul ℚ K'] [has_pow K' ℕ] [has_pow K' ℤ]
-  [has_nat_cast K'] [has_int_cast K'] [has_rat_cast K']
+  [has_div K'] [has_smul ℕ K'] [has_smul ℤ K'] [has_smul ℚ≥0 K'] [has_smul ℚ K'] [has_pow K' ℕ]
+  [has_pow K' ℤ] [has_nat_cast K'] [has_int_cast K'] [has_nnrat_cast K'] [has_rat_cast K']
   (f : K' → K) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
   (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
   (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
   (inv : ∀ x, f (x⁻¹) = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
   (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ x (n : ℤ), f (n • x) = n • f x)
-  (qsmul : ∀ x (n : ℚ), f (n • x) = n • f x)
+  (nnqsmul : ∀ x (q : ℚ≥0), f (q • x) = q • f x) (qsmul : ∀ x (q : ℚ), f (q • x) = q • f x)
   (npow : ∀ x (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ x (n : ℤ), f (x ^ n) = f x ^ n)
-  (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) (rat_cast : ∀ n : ℚ, f n = n) :
+  (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) (nnrat_cast : ∀ q : ℚ≥0, f q = q)
+  (rat_cast : ∀ q : ℚ, f q = q) :
   field K' :=
 { rat_cast := coe,
   rat_cast_mk := λ a b h1 h2, hf (by erw [rat_cast, mul, inv, int_cast, nat_cast];
                                      exact division_ring.rat_cast_mk a b h1 h2),
   qsmul := (•),
   qsmul_eq_mul' := λ a x, hf (by erw [qsmul, mul, rat.smul_def, rat_cast]),
-  .. hf.comm_group_with_zero f zero one mul inv div npow zpow,
+  .. hf.division_semiring f zero one add mul inv div nsmul nnqsmul npow zpow nat_cast nnrat_cast,
   .. hf.comm_ring f zero one add mul neg sub nsmul zsmul npow nat_cast int_cast }
 
 /-! ### Order dual -/
 
+instance [h : has_nnrat_cast α] : has_nnrat_cast αᵒᵈ := h
 instance [h : has_rat_cast α] : has_rat_cast αᵒᵈ := h
 instance [h : division_semiring α] : division_semiring αᵒᵈ := h
 instance [h : division_ring α] : division_ring αᵒᵈ := h
 instance [h : semifield α] : semifield αᵒᵈ := h
 instance [h : field α] : field αᵒᵈ := h
 
-@[simp] lemma to_dual_rat_cast [has_rat_cast α] (n : ℚ) : to_dual (n : α) = n := rfl
-@[simp] lemma of_dual_rat_cast [has_rat_cast α] (n : ℚ) : (of_dual n : α) = n := rfl
+@[simp] lemma to_dual_nnrat_cast [has_nnrat_cast α] (q : ℚ≥0) : to_dual (q : α) = q := rfl
+@[simp] lemma of_dual_nnrat_cast [has_nnrat_cast α] (q : ℚ≥0) : (of_dual ↑q : α) = q := rfl
+@[simp] lemma to_dual_rat_cast [has_rat_cast α] (q : ℚ) : to_dual (q : α) = q := rfl
+@[simp] lemma of_dual_rat_cast [has_rat_cast α] (q : ℚ) : (of_dual q : α) = q := rfl
 
 /-! ### Lexicographic order -/
 
+instance [h : has_nnrat_cast α] : has_nnrat_cast (lex α) := h
 instance [h : has_rat_cast α] : has_rat_cast (lex α) := h
 instance [h : division_semiring α] : division_semiring (lex α) := h
 instance [h : division_ring α] : division_ring (lex α) := h
 instance [h : semifield α] : semifield (lex α) := h
 instance [h : field α] : field (lex α) := h
 
-@[simp] lemma to_lex_rat_cast [has_rat_cast α] (n : ℚ) : to_lex (n : α) = n := rfl
-@[simp] lemma of_lex_rat_cast [has_rat_cast α] (n : ℚ) : (of_lex n : α) = n := rfl
+@[simp] lemma to_lex_nnrat_cast [has_nnrat_cast α] (q : ℚ≥0) : to_lex (q : α) = q := rfl
+@[simp] lemma of_lex_nnrat_cast [has_nnrat_cast α] (q : ℚ≥0) : (of_lex ↑q : α) = q := rfl
+@[simp] lemma to_lex_rat_cast [has_rat_cast α] (q : ℚ) : to_lex (q : α) = q := rfl
+@[simp] lemma of_lex_rat_cast [has_rat_cast α] (q : ℚ) : (of_lex q : α) = q := rfl

src/algebra/field/defs.lean

@@ -3,8 +3,8 @@ Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 -/
-import data.rat.init
 import algebra.ring.defs
+import data.rat.nnrat.defs
 
 /-!
 # Division (semi)rings and (semi)fields
@@ -47,6 +47,7 @@ field, division ring, skew field, skew-field, skewfield
 -/
 
 open function set
+open_locale nnrat
 
 set_option old_structure_cmd true
 
@@ -57,8 +58,8 @@ variables {α β K : Type*}
 is defined as `(a / b : K) = (a : K) * (b : K)⁻¹`.
 Use `coe` instead of `rat.cast_rec` for better definitional behaviour.
 -/
-def rat.cast_rec [has_lift_t ℕ K] [has_lift_t ℤ K] [has_mul K] [has_inv K] : ℚ → K
-| ⟨a, b, _, _⟩ := ↑a * (↑b)⁻¹
+def rat.cast_rec [has_lift_t ℕ K] [has_lift_t ℤ K] [has_mul K] [has_inv K] : ℚ → K :=
+λ q, ↑q.1 * (↑q.2)⁻¹
 
 /--
 Type class for the canonical homomorphism `ℚ → K`.
@@ -67,6 +68,17 @@ Type class for the canonical homomorphism `ℚ → K`.
 class has_rat_cast (K : Type u) :=
 (rat_cast : ℚ → K)
 
+/-- Construct the canonical injection from `ℚ` into an arbitrary division ring. If the field has
+positive characteristic `p`, we define `1 / p = 1 / 0 = 0` for consistency with our division by zero
+convention. -/
+@[priority 900] -- see Note [coercion into rings]
+instance rat.cast_coe {K : Type*} [has_rat_cast K] : has_coe_t ℚ K := ⟨has_rat_cast.rat_cast⟩
+
+/-- The default definition of the scalar multiplication `(a : ℚ≥0) • (x : K)` for a division
+semiring `K` is given by `a • x = (↑ a) * x`.
+Use `(a : ℚ≥0) • (x : K)` instead of `qsmul_rec` for better definitional behaviour. -/
+def nnqsmul_rec (coe : ℚ≥0 → K) [has_mul K] (a : ℚ≥0) (x : K) : K := coe a * x
+
 /-- The default definition of the scalar multiplication `(a : ℚ) • (x : K)` for a division ring `K`
 is given by `a • x = (↑ a) * x`.
 Use `(a : ℚ) • (x : K)` instead of `qsmul_rec` for better definitional behaviour.
@@ -76,7 +88,11 @@ coe a * x
 
 /-- A `division_semiring` is a `semiring` with multiplicative inverses for nonzero elements. -/
 @[protect_proj, ancestor semiring group_with_zero]
-class division_semiring (α : Type*) extends semiring α, group_with_zero α
+class division_semiring (α : Type u) extends semiring α, group_with_zero α, has_nnrat_cast α :=
+(nnrat_cast := nnrat.cast_rec)
+(nnrat_cast_eq : ∀ q, nnrat_cast q = q.num / q.denom . try_refl_tac)
+(nnqsmul : ℚ≥0 → α → α := nnqsmul_rec nnrat_cast)
+(nnqsmul_eq_mul : ∀ a x, nnqsmul a x = nnrat_cast a * x . try_refl_tac)
 
 /-- A `division_ring` is a `ring` with multiplicative inverses for nonzero elements.
 
@@ -89,9 +105,14 @@ definitions for some special cases of `K` (in particular `K = ℚ` itself).
 See also Note [forgetful inheritance].
 -/
 @[protect_proj, ancestor ring div_inv_monoid nontrivial]
-class division_ring (K : Type u) extends ring K, div_inv_monoid K, nontrivial K, has_rat_cast K :=
+class division_ring (K : Type u)
+  extends ring K, div_inv_monoid K, nontrivial K, has_nnrat_cast K, has_rat_cast K :=
 (mul_inv_cancel : ∀ {a : K}, a ≠ 0 → a * a⁻¹ = 1)
 (inv_zero : (0 : K)⁻¹ = 0)
+(nnrat_cast := nnrat.cast_rec)
+(nnrat_cast_eq : ∀ q, nnrat_cast q = q.num / q.denom . try_refl_tac)
+(nnqsmul : ℚ≥0 → K → K := nnqsmul_rec nnrat_cast)
+(nnqsmul_eq_mul : ∀ a x, nnqsmul a x = nnrat_cast a * x . try_refl_tac)
 (rat_cast := rat.cast_rec)
 (rat_cast_mk : ∀ (a : ℤ) (b : ℕ) h1 h2, rat_cast ⟨a, b, h1, h2⟩ = a * b⁻¹ . try_refl_tac)
 (qsmul : ℚ → K → K := qsmul_rec rat_cast)
@@ -107,29 +128,31 @@ class semifield (α : Type*) extends comm_semiring α, division_semiring α, com
 
 /-- A `field` is a `comm_ring` with multiplicative inverses for nonzero elements.
 
-An instance of `field K` includes maps `of_rat : ℚ → K` and `qsmul : ℚ → K → K`.
-If the field has positive characteristic p, we define `of_rat (1 / p) = 1 / 0 = 0`
+An instance of `field K` includes maps `rat_cast : ℚ → K` and `qsmul : ℚ → K → K`.
+If the field has positive characteristic p, we define `rat_cast (1 / p) = 1 / 0 = 0`
 for consistency with our division by zero convention.
-The fields `of_rat` and `qsmul are needed to implement the
+The fields `rat_cast` and `qsmul are needed to implement the
 `algebra_rat [division_ring K] : algebra ℚ K` instance, since we need to control the specific
 definitions for some special cases of `K` (in particular `K = ℚ` itself).
 See also Note [forgetful inheritance].
 -/
 @[protect_proj, ancestor comm_ring div_inv_monoid nontrivial]
 class field (K : Type u) extends comm_ring K, division_ring K
 
-section division_ring
-variables [division_ring K] {a b : K}
+namespace nnrat
+variables [division_semiring α] {a : α}
 
-namespace rat
+lemma cast_def : ∀ q : ℚ≥0, (q : α) = q.num / q.denom := division_semiring.nnrat_cast_eq
+
+@[priority 100]
+instance division_semiring.to_has_nnqsmul : has_smul ℚ≥0 α := ⟨division_semiring.nnqsmul⟩
 
-/-- Construct the canonical injection from `ℚ` into an arbitrary
-  division ring. If the field has positive characteristic `p`,
-  we define `1 / p = 1 / 0 = 0` for consistency with our
-  division by zero convention. -/
--- see Note [coercion into rings]
-@[priority 900] instance cast_coe {K : Type*} [has_rat_cast K] : has_coe_t ℚ K :=
-⟨has_rat_cast.rat_cast⟩
+lemma smul_def : ∀ (q : ℚ≥0) (a : α), q • a = ↑q * a := division_semiring.nnqsmul_eq_mul
+
+end nnrat
+
+namespace rat
+variables [division_ring K] {a b : K}
 
 theorem cast_mk' (a b h1 h2) : ((⟨a, b, h1, h2⟩ : ℚ) : K) = a * b⁻¹ :=
 division_ring.rat_cast_mk _ _ _ _
@@ -138,15 +161,13 @@ theorem cast_def : ∀ (r : ℚ), (r : K) = r.num / r.denom
 | ⟨a, b, h1, h2⟩ := (cast_mk' _ _ _ _).trans (div_eq_mul_inv _ _).symm
 
 @[priority 100]
-instance smul_division_ring : has_smul ℚ K :=
+instance division_ring.to_has_qsmul : has_smul ℚ K :=
 ⟨division_ring.qsmul⟩
 
 lemma smul_def (a : ℚ) (x : K) : a • x = ↑a * x := division_ring.qsmul_eq_mul' a x
 
 end rat
 
-end division_ring
-
 section field
 
 variable [field K]

src/algebra/field/opposite.lean

@@ -13,28 +13,65 @@ import algebra.ring.opposite
 > Any changes to this file require a corresponding PR to mathlib4.
 -/
 
-variables (α : Type*)
+open_locale nnrat
+
+variables {α : Type*}
+
+namespace mul_opposite
+
+@[to_additive] instance [has_nnrat_cast α] : has_nnrat_cast αᵐᵒᵖ := ⟨λ n, op n⟩
+@[to_additive] instance [has_rat_cast α] : has_rat_cast αᵐᵒᵖ := ⟨λ n, op n⟩
+
+@[simp, norm_cast, to_additive]
+lemma op_nnrat_cast [has_nnrat_cast α] (q : ℚ≥0) : op (q : α) = q := rfl
+
+@[simp, norm_cast, to_additive]
+lemma unop_nnrat_cast [has_nnrat_cast α] (q : ℚ≥0) : unop (q : αᵐᵒᵖ) = q := rfl
+
+@[simp, norm_cast, to_additive]
+lemma op_rat_cast [has_rat_cast α] (q : ℚ) : op (q : α) = q := rfl
+
+@[simp, norm_cast, to_additive]
+lemma unop_rat_cast [has_rat_cast α] (q : ℚ) : unop (q : αᵐᵒᵖ) = q := rfl
 
 instance [division_semiring α] : division_semiring αᵐᵒᵖ :=
-{ .. mul_opposite.group_with_zero α, .. mul_opposite.semiring α }
+{ nnrat_cast := λ q, op q,
+  nnrat_cast_eq := λ q, by { rw [nnrat.cast_def, op_div, op_nat_cast, op_nat_cast, div_eq_mul_inv],
+    exact nat.commute_cast _ _ },
+  .. mul_opposite.group_with_zero α, .. mul_opposite.semiring α }
 
 instance [division_ring α] : division_ring αᵐᵒᵖ :=
-{ .. mul_opposite.group_with_zero α, .. mul_opposite.ring α }
+{ rat_cast := λ q, op q,
+  rat_cast_mk := λ a b hb h, by { rw [rat.cast_def, op_div, op_nat_cast, op_int_cast],
+    exact int.commute_cast _ _ },
+  ..mul_opposite.division_semiring, ..mul_opposite.ring α }
 
 instance [semifield α] : semifield αᵐᵒᵖ :=
-{ .. mul_opposite.division_semiring α, .. mul_opposite.comm_semiring α }
+{ ..mul_opposite.division_semiring, ..mul_opposite.comm_semiring α }
 
 instance [field α] : field αᵐᵒᵖ :=
-{ .. mul_opposite.division_ring α, .. mul_opposite.comm_ring α }
+{ ..mul_opposite.division_ring, ..mul_opposite.comm_ring α }
+
+end mul_opposite
+
+namespace add_opposite
 
 instance [division_semiring α] : division_semiring αᵃᵒᵖ :=
-{ ..add_opposite.group_with_zero α, ..add_opposite.semiring α }
+{ nnrat_cast := λ q, op q,
+  nnrat_cast_eq := λ q, by { rw [nnrat.cast_def, op_div, op_nat_cast, op_nat_cast] },
+  ..add_opposite.group_with_zero α, ..add_opposite.semiring α, ..add_opposite.has_nnrat_cast }
 
 instance [division_ring α] : division_ring αᵃᵒᵖ :=
-{ ..add_opposite.group_with_zero α, ..add_opposite.ring α }
+{ nnrat_cast := coe,
+  nnrat_cast_eq := λ q, unop_injective q.cast_def,
+  nnqsmul := λ q a, op $ q • unop a,
+  nnqsmul_eq_mul := λ q a, by simp only [nnrat.smul_def, op_mul, op_nnrat_cast, op_unop],
+  ..add_opposite.group_with_zero α, ..add_opposite.ring α }
 
 instance [semifield α] : semifield αᵃᵒᵖ :=
-{ ..add_opposite.division_semiring α, ..add_opposite.comm_semiring α }
+{ ..add_opposite.division_semiring, ..add_opposite.comm_semiring α }
 
 instance [field α] : field αᵃᵒᵖ :=
-{ ..add_opposite.division_ring α, ..add_opposite.comm_ring α }
+{ ..add_opposite.division_ring, ..add_opposite.comm_ring α }
+
+end add_opposite