From a9f671a200ce53b15692df25952d7e6ebfebc9de Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Fri, 21 Aug 2026 23:50:34 -0400 Subject: [PATCH 1/7] prove instances --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index 8540e63c296d59..46b1fd3479a138 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3891,6 +3891,7 @@ public import Mathlib.Data.DFinsupp.Small public import Mathlib.Data.DFinsupp.Submonoid public import Mathlib.Data.DFinsupp.WellFounded public import Mathlib.Data.DList.Instances +public import Mathlib.Data.Dyadic.OrderedRing public import Mathlib.Data.ENNReal.Action public import Mathlib.Data.ENNReal.Basic public import Mathlib.Data.ENNReal.BigOperators From e204c7793dcf1b3c12aab090905cf257a7b8be9c Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Fri, 21 Aug 2026 23:52:00 -0400 Subject: [PATCH 2/7] git add --- Mathlib/Data/Dyadic/OrderedRing.lean | 159 +++++++++++++++++++++++++++ 1 file changed, 159 insertions(+) create mode 100644 Mathlib/Data/Dyadic/OrderedRing.lean diff --git a/Mathlib/Data/Dyadic/OrderedRing.lean b/Mathlib/Data/Dyadic/OrderedRing.lean new file mode 100644 index 00000000000000..0c37510aa31f4a --- /dev/null +++ b/Mathlib/Data/Dyadic/OrderedRing.lean @@ -0,0 +1,159 @@ +/- +Copyright (c) 2026 Aaron Liu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Aaron Liu +-/ +module + +public import Mathlib.Algebra.Order.Ring.Basic + +/-! +# Dyadic rationals form an ordered ring + +We provide instances of `LinearOrder Dyadic`, `CommRing Dyadic`, and `IsOrderedRing Dyadic`. +-/ + +public section +namespace Dyadic + +section Lemmas + +@[simp] theorem toRat_one : toRat 1 = 1 := rfl + +@[simp] protected theorem natCast_zero : (Nat.cast 0 : Dyadic) = 0 := rfl +@[simp] protected theorem natCast_one : (Nat.cast 1 : Dyadic) = 1 := rfl + +@[simp, norm_cast] +protected theorem natCast_add (a b : ℕ) : (Nat.cast (a + b) : Dyadic) = a + b := by + simp [← Dyadic.toRat_inj] + +@[simp] protected theorem intCast_zero : (Int.cast 0 : Dyadic) = 0 := rfl + +@[simp] protected theorem intCast_one : (Int.cast 1 : Dyadic) = 1 := rfl + +@[simp, norm_cast] +protected theorem intCast_add (a b : ℤ) : (Int.cast (a + b) : Dyadic) = a + b := by + simp [← Dyadic.toRat_inj] + +@[simp, norm_cast] +theorem intCast_natCast (n : ℕ) : (Int.cast n : Dyadic) = n := rfl + +@[simp, norm_cast] +protected theorem intCast_neg (a : Int) : ((-a : Int) : Dyadic) = -(a : Dyadic) := by + simp [← Dyadic.toRat_inj] + +end Lemmas + +section Instances + +instance : LinearOrder Dyadic where + le_refl := Dyadic.le_refl + le_trans := @Dyadic.le_trans + lt_iff_le_not_ge := Std.LawfulOrderLT.lt_iff + le_antisymm := @Dyadic.le_antisymm + le_total := Dyadic.le_total + toDecidableLE := inferInstance + toDecidableEq := inferInstance + toDecidableLT := inferInstance + +instance : CommRing Dyadic where + add_assoc := Dyadic.add_assoc + zero_add := Dyadic.zero_add + add_zero := Dyadic.add_zero + nsmul n x := n * x + nsmul_zero := by simp [· • ·, SMul.smul] + nsmul_succ := by simp [· • ·, SMul.smul, Dyadic.add_mul, Dyadic.one_mul] + add_comm := Dyadic.add_comm + mul_assoc := Dyadic.mul_assoc + one_mul := Dyadic.one_mul + mul_one := Dyadic.mul_one + npow_zero := Dyadic.pow_zero + npow_succ n x := Dyadic.pow_succ x n + zero_mul := Dyadic.zero_mul + mul_zero := Dyadic.mul_zero + left_distrib := Dyadic.mul_add + right_distrib := Dyadic.add_mul + natCast_zero := Dyadic.natCast_zero + natCast_succ := by simp + zsmul n x := n * x + sub_eq_add_neg _ _ := rfl + zsmul_zero' := by simp [· • ·, SMul.smul] + zsmul_succ' := by simp [· • ·, SMul.smul, Dyadic.add_mul, Dyadic.one_mul] + zsmul_neg' := by + intro n a + change (Int.negSucc n : ℤ) * a = -(n.succ * a) + rw [Int.negSucc_eq, Nat.succ_eq_add_one, ← toRat_inj, toRat_mul, toRat_intCast, toRat_neg, + toRat_mul, toRat_natCast, Rat.intCast_neg, Rat.intCast_add, Rat.intCast_natCast, + Rat.natCast_add, ← Rat.intCast_natCast 1, Int.natCast_one, Rat.neg_mul] + neg_add_cancel := Dyadic.neg_add_cancel + intCast_ofNat := Dyadic.intCast_natCast + intCast_negSucc := by + intro n + change Int.cast (Int.negSucc n) = -Nat.cast (n + 1) + rw [Int.negSucc_eq, ← toRat_inj, toRat_intCast, toRat_neg, toRat_natCast, Rat.intCast_neg, + Rat.intCast_add, Rat.intCast_natCast, Rat.natCast_add, ← Rat.intCast_natCast 1, + Int.natCast_one] + mul_comm := Dyadic.mul_comm + +instance : IsStrictOrderedRing Dyadic where + add_le_add_left := by simp [← Dyadic.toRat_le_toRat_iff, Rat.add_le_add_right] + add_le_add_right := by simp [← Dyadic.toRat_le_toRat_iff, Rat.add_le_add_left] + le_of_add_le_add_left := by simp [← Dyadic.toRat_le_toRat_iff, Rat.add_le_add_left] + le_of_add_le_add_right := by simp [← Dyadic.toRat_le_toRat_iff, Rat.add_le_add_right] + mul_lt_mul_of_pos_left := by simp +contextual [← Dyadic.toRat_lt_toRat_iff, Rat.mul_lt_mul_left] + mul_lt_mul_of_pos_right := by simp +contextual [← Dyadic.toRat_lt_toRat_iff, Rat.mul_lt_mul_right] + zero_le_one := by decide + exists_pair_ne := ⟨0, 1, by decide⟩ + +end Instances + +section Two + +@[expose, simps] +def twoUnit : Units Dyadic where + val := 2 + inv := (1 : Dyadic) >>> 1 + val_inv := rfl + inv_val := rfl + +theorem isUnit_iff_exists_twoUnit_pow {x : Dyadic} : IsUnit x ↔ ∃ n : ℤ, ↑(twoUnit ^ n) = x := by + refine ⟨fun hx => ?_, fun h => h.elim fun n hn => hn ▸ Units.isUnit (twoUnit ^ n)⟩ + rw [isUnit_iff_exists] at hx + obtain ⟨b, hxb, hbx⟩ := hx + cases x with | zero => simp at hxb | ofOdd nx kx hnx + cases b with | zero => simp at hxb | ofOdd nb kb hnb + refine ⟨-kx, ?_⟩ + rw [← toRat_inj, toRat_mul, toRat_ofOdd_eq_mkRat, toRat_ofOdd_eq_mkRat, toRat_one, + Rat.mkRat_mul_mkRat, ← Rat.intCast_one, ← Rat.mkRat_one, + Rat.mkRat_eq_iff (NeZero.ne _) (by decide), Int.natCast_one, Int.mul_one, Int.one_mul, + Nat.shiftLeft_eq, Nat.shiftLeft_eq, Nat.one_mul, Nat.one_mul, ← Nat.pow_add, + Int.natCast_pow, Nat.cast_ofNat, Int.shiftLeft_eq, Int.shiftLeft_eq, mul_mul_mul_comm, + ← Int.pow_add] at hxb + induction kx using Int.negInduction with + | nat kx => + rw [zpow_neg, zpow_natCast, ← inv_pow, Units.val_pow_eq_pow_val, val_inv_twoUnit] + change (ofOdd (1 ^ kx) (1 * kx) (by simp)) = ofOdd nx kx hnx + cases kb using Int.negInduction with + | nat kb => + simp_rw [Int.toNat_neg_natCast, Int.toNat_natCast, add_zero, pow_zero, Int.mul_one] at hxb + have hxb2 := congr($hxb % 2) + rw [Int.mul_emod, hnx, hnb, Int.mul_one, Int.one_emod_two] at hxb2 + cases kx with + | succ _ => rw [Nat.add_right_comm, pow_succ, Int.mul_emod_left] at hxb2; simp at hxb2 + | zero => + rw [zero_add] at hxb hxb2 + cases kb with + | succ _ => rw [pow_succ, Int.mul_emod_left] at hxb2; simp at hxb2 + | zero => + rw [pow_zero] at hxb + cases Int.mul_eq_one hxb + simp + + sorry + | neg _ kb => + sorry + | neg _ kx => sorry + +end Two + +end Dyadic From 1f662e65438a53f222695aaaddc0da8675081efb Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Sat, 22 Aug 2026 09:03:32 -0400 Subject: [PATCH 3/7] remove unfinished business --- Mathlib/Data/Dyadic/OrderedRing.lean | 49 ---------------------------- 1 file changed, 49 deletions(-) diff --git a/Mathlib/Data/Dyadic/OrderedRing.lean b/Mathlib/Data/Dyadic/OrderedRing.lean index 0c37510aa31f4a..022d67dacb31bc 100644 --- a/Mathlib/Data/Dyadic/OrderedRing.lean +++ b/Mathlib/Data/Dyadic/OrderedRing.lean @@ -107,53 +107,4 @@ instance : IsStrictOrderedRing Dyadic where end Instances -section Two - -@[expose, simps] -def twoUnit : Units Dyadic where - val := 2 - inv := (1 : Dyadic) >>> 1 - val_inv := rfl - inv_val := rfl - -theorem isUnit_iff_exists_twoUnit_pow {x : Dyadic} : IsUnit x ↔ ∃ n : ℤ, ↑(twoUnit ^ n) = x := by - refine ⟨fun hx => ?_, fun h => h.elim fun n hn => hn ▸ Units.isUnit (twoUnit ^ n)⟩ - rw [isUnit_iff_exists] at hx - obtain ⟨b, hxb, hbx⟩ := hx - cases x with | zero => simp at hxb | ofOdd nx kx hnx - cases b with | zero => simp at hxb | ofOdd nb kb hnb - refine ⟨-kx, ?_⟩ - rw [← toRat_inj, toRat_mul, toRat_ofOdd_eq_mkRat, toRat_ofOdd_eq_mkRat, toRat_one, - Rat.mkRat_mul_mkRat, ← Rat.intCast_one, ← Rat.mkRat_one, - Rat.mkRat_eq_iff (NeZero.ne _) (by decide), Int.natCast_one, Int.mul_one, Int.one_mul, - Nat.shiftLeft_eq, Nat.shiftLeft_eq, Nat.one_mul, Nat.one_mul, ← Nat.pow_add, - Int.natCast_pow, Nat.cast_ofNat, Int.shiftLeft_eq, Int.shiftLeft_eq, mul_mul_mul_comm, - ← Int.pow_add] at hxb - induction kx using Int.negInduction with - | nat kx => - rw [zpow_neg, zpow_natCast, ← inv_pow, Units.val_pow_eq_pow_val, val_inv_twoUnit] - change (ofOdd (1 ^ kx) (1 * kx) (by simp)) = ofOdd nx kx hnx - cases kb using Int.negInduction with - | nat kb => - simp_rw [Int.toNat_neg_natCast, Int.toNat_natCast, add_zero, pow_zero, Int.mul_one] at hxb - have hxb2 := congr($hxb % 2) - rw [Int.mul_emod, hnx, hnb, Int.mul_one, Int.one_emod_two] at hxb2 - cases kx with - | succ _ => rw [Nat.add_right_comm, pow_succ, Int.mul_emod_left] at hxb2; simp at hxb2 - | zero => - rw [zero_add] at hxb hxb2 - cases kb with - | succ _ => rw [pow_succ, Int.mul_emod_left] at hxb2; simp at hxb2 - | zero => - rw [pow_zero] at hxb - cases Int.mul_eq_one hxb - simp - - sorry - | neg _ kb => - sorry - | neg _ kx => sorry - -end Two - end Dyadic From 37d474f149d5ba4dbcd350edf257a9a8bda39d90 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Sat, 22 Aug 2026 09:31:28 -0400 Subject: [PATCH 4/7] simpNF --- Mathlib/Data/Dyadic/OrderedRing.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/Mathlib/Data/Dyadic/OrderedRing.lean b/Mathlib/Data/Dyadic/OrderedRing.lean index 022d67dacb31bc..f93dccac32b4fe 100644 --- a/Mathlib/Data/Dyadic/OrderedRing.lean +++ b/Mathlib/Data/Dyadic/OrderedRing.lean @@ -18,12 +18,14 @@ namespace Dyadic section Lemmas +-- Some of these lemmas are high priority then the generic ring lemmas so that the `simpNF` is happy + @[simp] theorem toRat_one : toRat 1 = 1 := rfl @[simp] protected theorem natCast_zero : (Nat.cast 0 : Dyadic) = 0 := rfl @[simp] protected theorem natCast_one : (Nat.cast 1 : Dyadic) = 1 := rfl -@[simp, norm_cast] +@[simp high, norm_cast] protected theorem natCast_add (a b : ℕ) : (Nat.cast (a + b) : Dyadic) = a + b := by simp [← Dyadic.toRat_inj] @@ -31,14 +33,14 @@ protected theorem natCast_add (a b : ℕ) : (Nat.cast (a + b) : Dyadic) = a + b @[simp] protected theorem intCast_one : (Int.cast 1 : Dyadic) = 1 := rfl -@[simp, norm_cast] +@[simp high, norm_cast] protected theorem intCast_add (a b : ℤ) : (Int.cast (a + b) : Dyadic) = a + b := by simp [← Dyadic.toRat_inj] @[simp, norm_cast] theorem intCast_natCast (n : ℕ) : (Int.cast n : Dyadic) = n := rfl -@[simp, norm_cast] +@[simp high, norm_cast] protected theorem intCast_neg (a : Int) : ((-a : Int) : Dyadic) = -(a : Dyadic) := by simp [← Dyadic.toRat_inj] From 1ed1eb53767eaa87fa86b07450ad293a4c5027c1 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Sat, 22 Aug 2026 12:34:39 -0400 Subject: [PATCH 5/7] prove theorem --- Mathlib.lean | 1 + Mathlib/Data/Dyadic/IsLocalization.lean | 92 +++++++++++++++++++++++++ 2 files changed, 93 insertions(+) create mode 100644 Mathlib/Data/Dyadic/IsLocalization.lean diff --git a/Mathlib.lean b/Mathlib.lean index 46b1fd3479a138..c52465e0f0d56a 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3891,6 +3891,7 @@ public import Mathlib.Data.DFinsupp.Small public import Mathlib.Data.DFinsupp.Submonoid public import Mathlib.Data.DFinsupp.WellFounded public import Mathlib.Data.DList.Instances +public import Mathlib.Data.Dyadic.IsLocalization public import Mathlib.Data.Dyadic.OrderedRing public import Mathlib.Data.ENNReal.Action public import Mathlib.Data.ENNReal.Basic diff --git a/Mathlib/Data/Dyadic/IsLocalization.lean b/Mathlib/Data/Dyadic/IsLocalization.lean new file mode 100644 index 00000000000000..08c8a422acdfd6 --- /dev/null +++ b/Mathlib/Data/Dyadic/IsLocalization.lean @@ -0,0 +1,92 @@ +/- +Copyright (c) 2026 Aaron Liu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Aaron Liu +-/ +module + +public import Mathlib.Algebra.Algebra.Basic +public import Mathlib.Data.Dyadic.OrderedRing +public import Mathlib.RingTheory.Localization.Defs + +/-! +# Dyadic rationals as a localization + +We prove `Dyadic` is the localization of `ℤ` at `Submonoid.powers 2`. +-/ + +public section +namespace Dyadic + +@[expose] +def half : Units Dyadic where + val := (1 : Dyadic) >>> 1 + inv := 2 + val_inv := rfl + inv_val := rfl + +-- `@[simps]` for `Units` is broken, see https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60.40.5Bsimps.5D.60.20for.20.60Units.60.20is.20broken/near/618107577 +@[simp] theorem val_inv_half : ↑(half⁻¹) = (2 : Dyadic) := rfl + +instance : Invertible (2 : Dyadic) where + invOf := half + invOf_mul_self := rfl + mul_invOf_self := rfl + +theorem val_half_eq_ofOdd : half = ofOdd 1 1 rfl := rfl +theorem val_half_zpow_eq_ofOdd (n : ℤ) : ↑(half ^ n) = ofOdd 1 n rfl := by + rw [← neg_neg n] + induction -n using Int.negInduction with + | nat n => + rw [zpow_neg, ← inv_zpow, zpow_natCast, Units.val_pow_eq_pow_val, val_inv_half, + ← Int.cast_ofNat (nat_lit 2), ← Int.cast_pow, + ← toRat_inj, toRat_intCast, toRat_ofOdd_eq_mul_two_pow, Int.cast_one, neg_neg, + zpow_natCast, Int.cast_pow, Int.cast_ofNat, Rat.one_mul] + | neg ih n => + rw [← Units.mul_left_inj (half ^ (-n : ℤ)), ← Units.val_mul, ← zpow_add, + Int.add_left_neg, zpow_zero, Units.val_one, ih] + change ofOdd 1 0 rfl = ofOdd .. + simp + +instance : IsLocalization (Submonoid.powers (2 : ℤ)) Dyadic where + map_units := by + simp_rw [Subtype.forall, Submonoid.mem_powers_iff, ← Set.mem_range, Set.forall_mem_range, + algebraMap_int_eq, Int.coe_castRingHom, Int.cast_pow, Int.cast_ofNat] + intro i + rw [← val_inv_half, ← Units.val_pow_eq_pow_val] + exact (half⁻¹ ^ i).isUnit + exists_of_eq := by simp [← SetLike.mem_coe, ← Set.nonempty_def] + surj := by + intro z + cases z with | zero => exact ⟨(0, 1), by simp⟩ | ofOdd n k hn + cases k with + | ofNat k => + refine ⟨(n, ⟨2 ^ k, (Submonoid.mem_powers_iff (2 ^ k) 2).2 ⟨k, rfl⟩⟩), ?_⟩ + rw [← toRat_inj, algebraMap_int_eq, Int.coe_castRingHom, toRat_intCast, + toRat_mul, toRat_intCast, Int.cast_pow, Int.cast_ofNat, + toRat_ofOdd_eq_mul_two_pow, Int.ofNat_eq_natCast, Rat.mul_assoc, + ← zpow_natCast, ← zpow_add₀ two_ne_zero, Int.add_left_neg, zpow_zero, Rat.mul_one] + | negSucc k => + refine ⟨(n * 2 ^ (k + 1), 1), ?_⟩ + rw [← toRat_inj, algebraMap_int_eq, Int.coe_castRingHom, toRat_intCast, + toRat_mul, toRat_intCast, Submonoid.coe_one, Int.cast_one, + toRat_ofOdd_eq_mul_two_pow, Int.neg_negSucc, zpow_natCast, Rat.mul_one, + Int.cast_mul, Int.cast_pow, Int.cast_ofNat] + +theorem isUnit_iff_exists_half_pow {x : Dyadic} : + IsUnit x ↔ ∃ n : ℤ, ↑(half ^ n) = x ∨ -↑(half ^ n) = x := by + refine ⟨fun hx => ?_, by rintro ⟨n, rfl | rfl⟩ <;> simp only [IsUnit.neg_iff, Units.isUnit]⟩ + rw [isUnit_iff_exists] at hx + obtain ⟨b, hxb, hbx⟩ := hx + cases x with | zero => simp at hxb | ofOdd nx kx hnx + cases b with | zero => simp at hxb | ofOdd nb kb hnb + refine ⟨kx, ?_⟩ + change ofOdd .. = ofOdd 1 0 rfl at hxb + injection hxb with hn hk + rcases Int.mul_eq_one_iff_eq_one_or_neg_one.1 hn with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ + · left + rw [val_half_zpow_eq_ofOdd] + · right + rw [val_half_zpow_eq_ofOdd, neg_ofOdd] + +end Dyadic From 8834d0df2c00f9447542c44d365b41afdf547153 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Sat, 22 Aug 2026 13:27:02 -0400 Subject: [PATCH 6/7] add docstring --- Mathlib/Data/Dyadic/IsLocalization.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Data/Dyadic/IsLocalization.lean b/Mathlib/Data/Dyadic/IsLocalization.lean index 08c8a422acdfd6..05a11c3376b56d 100644 --- a/Mathlib/Data/Dyadic/IsLocalization.lean +++ b/Mathlib/Data/Dyadic/IsLocalization.lean @@ -18,6 +18,7 @@ We prove `Dyadic` is the localization of `ℤ` at `Submonoid.powers 2`. public section namespace Dyadic +/-- The dyadic number ½. -/ @[expose] def half : Units Dyadic where val := (1 : Dyadic) >>> 1 From 933d5a26b326f5438e89e895a7cd7106e615530f Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Mon, 24 Aug 2026 14:01:40 -0400 Subject: [PATCH 7/7] unsimp instead --- Mathlib/Data/Dyadic/OrderedRing.lean | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/Mathlib/Data/Dyadic/OrderedRing.lean b/Mathlib/Data/Dyadic/OrderedRing.lean index f93dccac32b4fe..61a5f777ea905a 100644 --- a/Mathlib/Data/Dyadic/OrderedRing.lean +++ b/Mathlib/Data/Dyadic/OrderedRing.lean @@ -18,14 +18,12 @@ namespace Dyadic section Lemmas --- Some of these lemmas are high priority then the generic ring lemmas so that the `simpNF` is happy - @[simp] theorem toRat_one : toRat 1 = 1 := rfl @[simp] protected theorem natCast_zero : (Nat.cast 0 : Dyadic) = 0 := rfl @[simp] protected theorem natCast_one : (Nat.cast 1 : Dyadic) = 1 := rfl -@[simp high, norm_cast] +@[norm_cast] protected theorem natCast_add (a b : ℕ) : (Nat.cast (a + b) : Dyadic) = a + b := by simp [← Dyadic.toRat_inj] @@ -33,14 +31,14 @@ protected theorem natCast_add (a b : ℕ) : (Nat.cast (a + b) : Dyadic) = a + b @[simp] protected theorem intCast_one : (Int.cast 1 : Dyadic) = 1 := rfl -@[simp high, norm_cast] +@[norm_cast] protected theorem intCast_add (a b : ℤ) : (Int.cast (a + b) : Dyadic) = a + b := by simp [← Dyadic.toRat_inj] @[simp, norm_cast] theorem intCast_natCast (n : ℕ) : (Int.cast n : Dyadic) = n := rfl -@[simp high, norm_cast] +@[norm_cast] protected theorem intCast_neg (a : Int) : ((-a : Int) : Dyadic) = -(a : Dyadic) := by simp [← Dyadic.toRat_inj] @@ -64,7 +62,7 @@ instance : CommRing Dyadic where add_zero := Dyadic.add_zero nsmul n x := n * x nsmul_zero := by simp [· • ·, SMul.smul] - nsmul_succ := by simp [· • ·, SMul.smul, Dyadic.add_mul, Dyadic.one_mul] + nsmul_succ := by simp [· • ·, SMul.smul, Dyadic.add_mul, Dyadic.one_mul, Dyadic.natCast_add] add_comm := Dyadic.add_comm mul_assoc := Dyadic.mul_assoc one_mul := Dyadic.one_mul @@ -76,11 +74,11 @@ instance : CommRing Dyadic where left_distrib := Dyadic.mul_add right_distrib := Dyadic.add_mul natCast_zero := Dyadic.natCast_zero - natCast_succ := by simp + natCast_succ := by simp [Dyadic.natCast_add] zsmul n x := n * x sub_eq_add_neg _ _ := rfl zsmul_zero' := by simp [· • ·, SMul.smul] - zsmul_succ' := by simp [· • ·, SMul.smul, Dyadic.add_mul, Dyadic.one_mul] + zsmul_succ' := by simp [· • ·, SMul.smul, Dyadic.add_mul, Dyadic.one_mul, Dyadic.intCast_add] zsmul_neg' := by intro n a change (Int.negSucc n : ℤ) * a = -(n.succ * a)