From 3c3cc7961266b5ec65e186a6d449f333eab00902 Mon Sep 17 00:00:00 2001
From: Ashvni <ashvni.n@gmail.com>
Date: Fri, 5 May 2023 17:15:52 +0100
Subject: [PATCH 1/9] changed to appropriate locations

---
 src/data/zmod/basic.lean                |  83 +++++++++++
 src/data/zmod/crt_properties.lean       |  89 ++++++++++++
 src/data/zmod/units.lean                | 174 ++++++++++++++++++++++++
 src/topology/algebra/constructions.lean |  36 +++++
 src/topology/maps.lean                  |   7 +
 5 files changed, 389 insertions(+)
 create mode 100644 src/data/zmod/crt_properties.lean
 create mode 100644 src/data/zmod/units.lean

diff --git a/src/data/zmod/basic.lean b/src/data/zmod/basic.lean
index 807cd3aff05e8..f7c3820b1c631 100644
--- a/src/data/zmod/basic.lean
+++ b/src/data/zmod/basic.lean
@@ -751,6 +751,75 @@ end
 lemma val_cast_of_lt {n : ℕ} {a : ℕ} (h : a < n) : (a : zmod n).val = a :=
 by rw [val_nat_cast, nat.mod_eq_of_lt h]
 
+lemma val_le_self (a n : ℕ) : (a : zmod n).val ≤ a :=
+begin
+  cases n,
+  { refl, },
+  { by_cases a < n.succ,
+    { rw zmod.val_cast_of_lt h, },
+    { apply le_trans (zmod.val_le _) (le_of_not_gt h), }, },
+end
+
+lemma val_coe_val_le_val {n m : ℕ} [ne_zero m] (y : zmod n) : (y.val : zmod m).val ≤ y.val :=
+begin
+  by_cases y.val < m,
+  { rw zmod.val_cast_of_lt h, },
+  { apply le_of_lt (gt_of_ge_of_gt (not_lt.1 h) (zmod.val_lt (y.val : zmod m))), },
+end
+
+lemma val_coe_val_le_val' {n m : ℕ} [ne_zero m] [ne_zero n] (y : zmod n) :
+  (y : zmod m).val ≤ y.val := (@zmod.nat_cast_val _ (zmod m) _ _ y) ▸ val_coe_val_le_val y
+
+lemma coe_val_eq_val_of_lt {n m : ℕ} [ne_zero n] (h : n < m) (b : zmod n) :
+  (b.val : zmod m).val = b.val :=
+begin
+  have h2 : b.val = (b : zmod m).val,
+  { rw ←zmod.val_cast_of_lt (lt_trans (zmod.val_lt b) h),
+    refine congr_arg _ (zmod.nat_cast_val _), },
+  conv_rhs { rw h2, },
+  refine congr_arg _ _,
+  rwa zmod.nat_cast_val _,
+end
+
+lemma zero_le_div_and_div_lt_one {n : ℕ} [ne_zero n] (x : zmod n) :
+  0 ≤ (x.val : ℚ) / n ∧ (x.val : ℚ) / n < 1 :=
+⟨div_nonneg (nat.cast_le.2 (nat.zero_le _)) (nat.cast_le.2 (nat.zero_le _)), (div_lt_one
+  $ by {refine nat.cast_pos.2 (ne_zero.pos _)}).2 -- removing the by and refine does not work?
+    (nat.cast_lt.2 (zmod.val_lt _))⟩
+
+lemma nat_cast_zmod_cast_int {n a : ℕ} (h : a < n) : ((a : zmod n) : ℤ) = (a : ℤ) :=
+begin
+  by_cases h' : 0 < n,
+  { rw ←zmod.nat_cast_val _,
+    { apply congr rfl (zmod.val_cast_of_lt h), },
+    { apply ne_zero.of_pos h', }, },
+  simp only [not_lt, _root_.le_zero_iff] at h',
+  rw h',
+  simp only [zmod.cast_id', id.def],
+end
+
+lemma cast_int_one {n : ℕ} [fact (1 < n)] : ((1 : zmod n) : ℤ) = 1 :=
+begin
+  rwa [←zmod.nat_cast_val _, zmod.val_one _],
+  simp only [int.coe_nat_zero, int.coe_nat_succ, zero_add],
+  { assumption, },
+  { refine ⟨ne_zero_of_lt (fact.out (1 < n))⟩, },
+end
+
+lemma cast_nat_eq_zero_of_dvd {m n : ℕ} (h : m ∣ n) : (n : zmod m) = 0 :=
+begin
+  rw [←zmod.cast_nat_cast h, zmod.nat_cast_self, zmod.cast_zero],
+  refine zmod.char_p _,
+end
+
+lemma dvd_val_sub_cast_val {m : ℕ} (n : ℕ) [ne_zero m] [ne_zero n] (a : zmod m) :
+  n ∣ a.val - (a : zmod n).val :=
+begin
+  have : (a.val : zmod n) = ((a : zmod n).val : zmod n),
+  { rw [nat_cast_val, nat_cast_val], norm_cast, },
+  exact nat.dvd_iff_mod_eq_zero.2 (nat.sub_mod_eq_zero_of_mod_eq ((eq_iff_modeq_nat _).1 this)),
+end
+
 lemma neg_val' {n : ℕ} [ne_zero n] (a : zmod n) : (-a).val = (n - a.val) % n :=
 calc (-a).val = val (-a)    % n : by rw nat.mod_eq_of_lt ((-a).val_lt)
           ... = (n - val a) % n : nat.modeq.add_right_cancel' _ (by rw [nat.modeq, ←val_add,
@@ -1021,6 +1090,20 @@ instance subsingleton_ring_equiv [semiring R] : subsingleton (zmod n ≃+* R) :=
   f k = k :=
 by { cases n; simp }
 
+lemma cast_eq_of_dvd {m n : ℕ} (h : m ∣ n) (a : zmod m) : ((a : zmod n) : zmod m) = a :=
+begin
+  conv_rhs { rw ←zmod.ring_hom_map_cast (zmod.cast_hom h (zmod m)) a, },
+  rw zmod.cast_hom_apply,
+end
+
+@[simp]
+lemma cast_hom_self {n : ℕ} : zmod.cast_hom dvd_rfl (zmod n) = ring_hom.id (zmod n) := by simp
+
+@[simp]
+lemma cast_hom_comp {n m d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
+  (zmod.cast_hom hm (zmod n)).comp (zmod.cast_hom hd (zmod m)) = zmod.cast_hom (dvd_trans hm hd) (zmod n) :=
+ring_hom.ext_zmod _ _
+
 lemma ring_hom_right_inverse [ring R] (f : R →+* (zmod n)) :
   function.right_inverse (coe : zmod n → R) f :=
 ring_hom_map_cast f
diff --git a/src/data/zmod/crt_properties.lean b/src/data/zmod/crt_properties.lean
new file mode 100644
index 0000000000000..37d22503fea43
--- /dev/null
+++ b/src/data/zmod/crt_properties.lean
@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2023 Ashvni Narayanan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ashvni Narayanan
+-/
+import data.zmod.basic
+import number_theory.padics.ring_homs
+
+/-!
+# Properties of ℤ/nℤ for the Chinese Remainder Theorem
+
+This file has some theorems regarding coercions with respect to the Chinese Remainder Theorem for
+`zmod n` for all `n`.
+
+## Main definitions and theorems
+ * `proj_fst`, `proj_snd`, `inv_fst`, `inv_snd` : lemmas regarding CRT
+
+## Tags
+zmod, CRT
+-/
+
+lemma proj_fst' {m n : ℕ} (h : m.coprime n) (a : zmod m) (b : zmod n) :
+  zmod.cast_hom (show m ∣ m * n, from dvd.intro n rfl) (zmod m)
+    ((zmod.chinese_remainder h).symm (a,b)) = a :=
+begin
+  change _ = prod.fst (a, b),
+  have h2 : zmod.cast_hom (show m.lcm n ∣ m * n, by simp [nat.lcm_dvd_iff]) (zmod m × zmod n) _ = _,
+    exact (zmod.chinese_remainder h).right_inv (a,b),
+  conv_rhs { rw ←h2, },
+  convert_to _ = (ring_hom.comp (ring_hom.fst (zmod m) (zmod n))
+    (zmod.cast_hom _ (zmod m × zmod n))) ((zmod.chinese_remainder h).inv_fun (a, b)) using 1,
+  apply congr _ rfl, congr,
+  refine ring_hom.ext_zmod _ _,
+end
+
+lemma proj_snd' {m n : ℕ} (h : m.coprime n) (a : zmod m) (b : zmod n) :
+  zmod.cast_hom (show n ∣ m * n, from dvd.intro_left m rfl) (zmod n)
+    ((zmod.chinese_remainder h).symm (a,b)) = b :=
+begin
+  change _ = prod.snd (a, b),
+  have h2 : zmod.cast_hom (show m.lcm n ∣ m * n, by simp [nat.lcm_dvd_iff]) (zmod m × zmod n) _ = _,
+    exact (zmod.chinese_remainder h).right_inv (a,b),
+  conv_rhs { rw ←h2, },
+  convert_to _ = (ring_hom.comp (ring_hom.snd (zmod m) (zmod n))
+    (zmod.cast_hom _ (zmod m × zmod n))) ((zmod.chinese_remainder h).inv_fun (a, b)) using 1,
+  apply congr _ rfl, congr,
+  refine ring_hom.ext_zmod _ _,
+end
+
+open zmod
+lemma inv_fst' {m n : ℕ} (x : zmod (m * n)) (cop : m.coprime n) :
+  (((zmod.chinese_remainder cop).to_equiv) x).fst = (x : zmod m) :=
+by { simp only [zmod.chinese_remainder, ring_equiv.to_equiv_eq_coe, ring_equiv.coe_to_equiv,
+  ring_equiv.coe_mk, cast_hom_apply, prod.fst_zmod_cast]}
+-- takes a long time to compile if not squeezed
+
+lemma inv_snd' {m n : ℕ} (x : zmod (m * n)) (cop : m.coprime n) :
+  (((zmod.chinese_remainder cop).to_equiv) x).snd = (x : zmod n) :=
+by { simp only [zmod.chinese_remainder, ring_equiv.to_equiv_eq_coe, ring_equiv.coe_to_equiv,
+  ring_equiv.coe_mk, zmod.cast_hom_apply, prod.snd_zmod_cast], }
+
+variables {p : ℕ} {d : ℕ}
+open padic_int
+
+lemma proj_fst [fact p.prime] {n : ℕ} (x : zmod d × ℤ_[p]) (cop : d.coprime (p^n)) :
+  ↑((zmod.chinese_remainder cop).symm (x.fst, (to_zmod_pow n) x.snd)) = x.fst := proj_fst' _ _ _
+
+lemma proj_snd [fact p.prime] {n : ℕ} (x : zmod d × ℤ_[p]) (cop : d.coprime (p^n)) :
+  ↑((zmod.chinese_remainder cop).symm (x.fst, (to_zmod_pow n) x.snd)) =
+  (to_zmod_pow n) x.snd :=
+proj_snd' _ _ _
+
+lemma inv_fst {n : ℕ} (x : zmod (d * p^n)) (cop : d.coprime (p^n)) :
+  (((zmod.chinese_remainder cop).to_equiv) x).fst = (x : zmod d) := inv_fst' x _
+
+lemma inv_snd {n : ℕ} (x : zmod (d * p^n)) (cop : d.coprime (p^n)) :
+  (((zmod.chinese_remainder cop).to_equiv) x).snd = (x : zmod (p^n)) := inv_snd' _ _
+
+variable (p)
+lemma proj_fst'' {n : ℕ} (hd : d.coprime p) (a : (zmod d)ˣ × (zmod (p^n))ˣ) :
+((zmod.chinese_remainder (nat.coprime.pow_right n hd)).inv_fun (↑(a.fst), ↑(a.snd)) : zmod d) = a.fst :=
+by { rw ring_equiv.inv_fun_eq_symm, apply proj_fst', }
+
+lemma proj_snd'' [fact p.prime] {n : ℕ} (hd : d.coprime p) (a : (zmod d)ˣ × (zmod (p^n))ˣ) :
+(padic_int.to_zmod_pow n) ((zmod.chinese_remainder (nat.coprime.pow_right n hd)).inv_fun (↑(a.fst), ↑(a.snd)) : ℤ_[p]) = a.snd :=
+begin
+  rw [← zmod.int_cast_cast, map_int_cast, zmod.int_cast_cast, ring_equiv.inv_fun_eq_symm],
+  convert proj_snd' _ _ _,
+end
diff --git a/src/data/zmod/units.lean b/src/data/zmod/units.lean
new file mode 100644
index 0000000000000..825cec5193273
--- /dev/null
+++ b/src/data/zmod/units.lean
@@ -0,0 +1,174 @@
+/-
+Copyright (c) 2023 Ashvni Narayanan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ashvni Narayanan
+-/
+import data.zmod.basic
+import data.zmod.topology
+
+/-!
+# Properties of units of ℤ/nℤ
+
+This file enlists some properties of units of `zmod n`. We then define a topological structure
+(the discrete topology) on `zmod n` for all `n` and consequently on the units.
+We also enlist several properties that are helpful with modular arithmetic.
+
+## Main definitions and theorems
+ * `zmod.topological_space`
+ * `cast_hom_apply'` : a version of `cast_hom_apply` where `R` is explicit
+ * `disc_top_units` : giving discrete topology to `units (zmod n)`
+
+## Tags
+zmod, units
+-/
+
+open zmod nat
+namespace zmod
+/-- Same as `zmod.cast_hom_apply` with some hypotheses being made explicit. -/
+lemma cast_hom_apply' {n : ℕ} (R : Type*) [_inst_1 : ring R] {m : ℕ} [_inst_2 : char_p R m]
+  (h : m ∣ n) (i : zmod n) : (cast_hom h R) i = ↑i := cast_hom_apply i
+
+lemma coe_map_of_dvd {a b : ℕ} (h : a ∣ b) (x : units (zmod b)) :
+  is_unit (x : zmod a) :=
+begin
+  change is_unit ((x : zmod b) : zmod a),
+  rw [←zmod.cast_hom_apply' (zmod a) h (x : zmod b), ←ring_hom.coe_monoid_hom, ←units.coe_map],
+  apply units.is_unit,
+end
+
+lemma is_unit_of_is_coprime_dvd {a b : ℕ} (h : a ∣ b) {x : ℕ} (hx : x.coprime b) :
+  is_unit (x : zmod a) :=
+begin
+  convert_to is_unit ((zmod.unit_of_coprime _ hx : zmod b) : zmod a),
+  { rw ←cast_nat_cast h x,
+    { congr, },
+    { refine zmod.char_p _, }, },
+  { apply coe_map_of_dvd h _, },
+end
+
+lemma is_unit_mul {a b g : ℕ} (n : ℕ) (h1 : g.coprime a) (h2 : g.coprime b) :
+  is_unit (g : zmod (a * b^n)) :=
+is_unit_of_is_coprime_dvd dvd_rfl ((coprime.mul_right h1 (coprime.pow_right _ h2)))
+
+lemma cast_inv {a m n : ℕ} (ha : a.coprime n) (h : m ∣ n) :
+  (((a : zmod n)⁻¹ : zmod n) : zmod m) = ((a : zmod n) : zmod m)⁻¹ :=
+begin
+  change ((((zmod.unit_of_coprime a ha)⁻¹ : units (zmod n)) : zmod n) : zmod m) = _,
+  have h1 : ∀ c : (zmod m)ˣ, (c : zmod m)⁻¹ = ((c⁻¹ : units (zmod m)) : zmod m),
+  { intro c, simp only [inv_coe_unit], },
+  rw [← zmod.cast_hom_apply' (zmod m) h _, ← ring_hom.coe_monoid_hom,
+    ← units.coe_map_inv _ (zmod.unit_of_coprime a ha), ← h1],
+  congr,
+end
+
+lemma coprime_of_is_unit {m a : ℕ} (ha : is_unit (a : zmod m)) : a.coprime m :=
+begin
+  have f := zmod.val_coe_unit_coprime (is_unit.unit ha),
+  rw is_unit.unit_spec at f,
+  obtain ⟨y, hy⟩ : m ∣ (a - (a : zmod m).val),
+  { rw [← zmod.nat_coe_zmod_eq_zero_iff_dvd, nat.cast_sub (zmod.val_le_self _ _), sub_eq_zero],
+    cases m,
+    { simp only [int.coe_nat_inj'], refl, },
+    { rw zmod.nat_cast_val, simp only [zmod.cast_nat_cast'], }, },
+  rw nat.sub_eq_iff_eq_add (zmod.val_le_self _ _) at hy,
+  rw [hy, add_comm, ← nat.is_coprime_iff_coprime],
+  simp only [int.coe_nat_add, int.coe_nat_mul],
+  rw [is_coprime.add_mul_left_left_iff, nat.is_coprime_iff_coprime],
+  convert zmod.val_coe_unit_coprime (is_unit.unit ha),
+end
+
+instance units_fintype {n : ℕ} : fintype (zmod n)ˣ :=
+begin
+  by_cases n = 0,
+  { rw h, refine units_int.fintype, },
+  { haveI : ne_zero n := ⟨h⟩,
+    apply units.fintype, },
+end
+
+lemma is_unit_of_is_unit_mul {m n : ℕ} (x : ℕ) (hx : is_unit (x : zmod (m * n))) :
+  is_unit (x : zmod m) :=
+begin
+  rw is_unit_iff_dvd_one at *,
+  cases hx with k hk,
+  refine ⟨(k : zmod m), _⟩,
+  rw [← zmod.cast_nat_cast (dvd_mul_right m n), ← zmod.cast_mul (dvd_mul_right m n),
+   ← hk, zmod.cast_one (dvd_mul_right m n)],
+  any_goals { refine zmod.char_p _, },
+end
+
+lemma is_unit_of_is_unit_mul' {m n : ℕ} (x : ℕ) (hx : is_unit (x : zmod (m * n))) :
+  is_unit (x : zmod n) :=
+begin
+  rw mul_comm at hx,
+  apply is_unit_of_is_unit_mul x hx,
+end
+
+open zmod
+lemma is_unit_of_is_unit_mul_iff {m n : ℕ} (x : ℕ) : is_unit (x : zmod (m * n)) ↔
+  is_unit (x : zmod m) ∧ is_unit (x : zmod n) :=
+  ⟨λ h, ⟨is_unit_of_is_unit_mul x h, is_unit_of_is_unit_mul' x h⟩,
+   λ ⟨h1, h2⟩, units.is_unit (zmod.unit_of_coprime x (nat.coprime.mul_right
+      (coprime_of_is_unit h1) (coprime_of_is_unit h2))), ⟩
+
+lemma not_is_unit_of_not_is_unit_mul {m n x : ℕ} (hx : ¬ is_unit (x : zmod (m * n))) :
+  ¬ is_unit (x : zmod m) ∨ ¬ is_unit (x : zmod n) :=
+begin
+  rw ← not_and_distrib,
+  contrapose hx,
+  rw not_not at *,
+  rw is_unit_of_is_unit_mul_iff,
+  refine ⟨hx.1, hx.2⟩,
+end
+
+lemma not_is_unit_of_not_is_unit_mul' {m n : ℕ} [ne_zero (m * n)] (x : zmod (m * n))
+  (hx : ¬ is_unit x) : ¬ is_unit (x : zmod m) ∨ ¬ is_unit (x : zmod n) :=
+begin
+  rw [← zmod.cast_id _ x, ← zmod.nat_cast_val] at hx,
+  rw [← zmod.nat_cast_val, ← zmod.nat_cast_val],
+  apply not_is_unit_of_not_is_unit_mul hx,
+end
+
+lemma is_unit_val_of_unit {n k : ℕ} [ne_zero n] (hk : k ∣ n) (u : (zmod n)ˣ) :
+  is_unit ((u : zmod n).val : zmod k) :=
+by { apply zmod.is_unit_of_is_coprime_dvd hk (coprime_of_is_unit _),
+  rw [zmod.nat_cast_val, zmod.cast_id], apply units.is_unit _, }
+
+lemma unit_ne_zero {n : ℕ} [fact (1 < n)] (a : (zmod n)ˣ) : (a : zmod n).val ≠ 0 :=
+begin
+  intro h,
+  rw zmod.val_eq_zero at h,
+  have : is_unit (0 : zmod n),
+  { rw ← h, simp, },
+  rw is_unit_zero_iff at this,
+  apply @zero_ne_one _ _ _ _,
+  rw this,
+  apply_instance,
+end
+
+lemma inv_is_unit_of_is_unit {n : ℕ} {u : zmod n} (h : is_unit u) : is_unit u⁻¹ :=
+begin
+  have h' := is_unit_iff_dvd_one.1 h,
+  cases h' with k h',
+  rw is_unit_iff_dvd_one,
+  refine ⟨u, _⟩,
+  rw zmod.inv_mul_of_unit u h,
+end
+end zmod
+
+/-- Making `zmod` a discrete topological space. -/
+def zmod.topological_space (d : ℕ) : topological_space (zmod d) := ⊥
+
+local attribute [instance] zmod.topological_space
+instance {n : ℕ} : discrete_topology (zmod n) := ⟨rfl⟩
+
+namespace zmod
+@[continuity]
+lemma induced_top_cont_inv {n : ℕ} : @continuous _ _ (topological_space.induced
+  (units.coe_hom (zmod n)) infer_instance) _ (units.inv : (zmod n)ˣ → zmod n) :=
+units.induced_top_cont_inv
+
+instance {k : ℕ} : discrete_topology (zmod k)ˣ := units.discrete_topology_of_discrete
+
+instance discrete_prod_units {m n : ℕ} : discrete_topology (zmod m × zmod n)ˣ :=
+units.discrete_prod_units
+end zmod
diff --git a/src/topology/algebra/constructions.lean b/src/topology/algebra/constructions.lean
index 1d4aa52d818f3..73c46ac1efe15 100644
--- a/src/topology/algebra/constructions.lean
+++ b/src/topology/algebra/constructions.lean
@@ -115,4 +115,40 @@ by simp only [inducing_embed_product.continuous_iff, embed_product_apply, (∘),
 @[to_additive] lemma continuous_coe_inv : continuous (λ u, ↑u⁻¹ : Mˣ → M) :=
 (units.continuous_iff.1 continuous_id).2
 
+/-- The inverse map `units.inv` is continuous with respect to the topology induced by
+  `units.coe_hom` on units. -/
+@[continuity]
+lemma induced_top_cont_inv {X : Type*} [topological_space X] [discrete_topology X] [monoid X] :
+  @continuous _ _ (topological_space.induced (units.coe_hom X) infer_instance) _
+  (units.inv : Xˣ → X) :=
+begin
+  convert continuous_of_discrete_topology,
+  refine @inducing.discrete_topology Xˣ X (topological_space.induced
+    (units.coe_hom X) infer_instance) _ _ (units.coe_hom _)
+    (λ a b h, units.eq_iff.1 h) rfl,
+-- Alternate proof :
+--  refine @embedding.discrete_topology (zmod n)ˣ (zmod n) (topological_space.induced
+--    (units.coe_hom (zmod n)) infer_instance) _ _ (units.coe_hom _) _,
+--  constructor,
+--  { constructor, refl, },
+--  { refine λ a b h, units.eq_iff.1 h, }, }
+end
+
+lemma discrete_topology_of_discrete {X : Type*} [_root_.topological_space X] [discrete_topology X]
+  [monoid X] : discrete_topology Xˣ :=
+begin
+  convert embedding.discrete_topology units.embedding_embed_product,
+  apply @prod.discrete_topology _ _ infer_instance infer_instance infer_instance infer_instance,
+  swap, { refine embedding.discrete_topology (embedding.mk ⟨rfl⟩ mul_opposite.unop_injective), },
+  { apply_instance, },
+end
+
+lemma discrete_prod_units {X Y : Type*} [monoid X] [monoid Y] [topological_space X]
+  [discrete_topology X] [topological_space Y] [discrete_topology Y] : discrete_topology (X × Y)ˣ :=
+begin
+  apply @embedding.discrete_topology _ _ _ _ prod.discrete_topology (units.embed_product _)
+    (units.embedding_embed_product),
+  { apply_instance, },
+  { refine inducing.discrete_topology (mul_opposite.unop_injective) rfl, },
+end
 end units
diff --git a/src/topology/maps.lean b/src/topology/maps.lean
index 1f6641fd51246..6e940dbb56137 100644
--- a/src/topology/maps.lean
+++ b/src/topology/maps.lean
@@ -222,6 +222,13 @@ discrete_topology_iff_nhds.2 $ λ x, by rw [hf.nhds_eq_comap, nhds_discrete, com
 
 end embedding
 
+namespace inducing
+lemma discrete_topology {X Y : Type*} [h1 : _root_.topological_space X]
+  [h2 : _root_.topological_space Y] [discrete_topology Y] {f : X → Y} (inj : function.injective f)
+  (ind : h1 = topological_space.induced f h2) : discrete_topology X :=
+embedding.discrete_topology (embedding.mk ⟨ind⟩ inj)
+end inducing
+
 /-- A function between topological spaces is a quotient map if it is surjective,
   and for all `s : set β`, `s` is open iff its preimage is an open set. -/
 def quotient_map {α : Type*} {β : Type*} [tα : topological_space α] [tβ : topological_space β]

From b27f870f269c77c0373bd3539c950448dd888e69 Mon Sep 17 00:00:00 2001
From: Ashvni <ashvni.n@gmail.com>
Date: Fri, 5 May 2023 17:37:04 +0100
Subject: [PATCH 2/9] lint error

---
 src/data/zmod/basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/data/zmod/basic.lean b/src/data/zmod/basic.lean
index f7c3820b1c631..efb4891dcc7e0 100644
--- a/src/data/zmod/basic.lean
+++ b/src/data/zmod/basic.lean
@@ -1101,8 +1101,8 @@ lemma cast_hom_self {n : ℕ} : zmod.cast_hom dvd_rfl (zmod n) = ring_hom.id (zm
 
 @[simp]
 lemma cast_hom_comp {n m d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
-  (zmod.cast_hom hm (zmod n)).comp (zmod.cast_hom hd (zmod m)) = zmod.cast_hom (dvd_trans hm hd) (zmod n) :=
-ring_hom.ext_zmod _ _
+  (zmod.cast_hom hm (zmod n)).comp (zmod.cast_hom hd (zmod m)) = zmod.cast_hom (dvd_trans hm hd)
+  (zmod n) := ring_hom.ext_zmod _ _
 
 lemma ring_hom_right_inverse [ring R] (f : R →+* (zmod n)) :
   function.right_inverse (coe : zmod n → R) f :=

From 9ac7521503a9df4651977e4e33dc824cba8b056c Mon Sep 17 00:00:00 2001
From: Ashvni <ashvni.n@gmail.com>
Date: Fri, 5 May 2023 20:41:05 +0100
Subject: [PATCH 3/9] sorting out linter

---
 src/data/zmod/crt_properties.lean | 12 ++++++++----
 src/data/zmod/units.lean          |  2 +-
 2 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/data/zmod/crt_properties.lean b/src/data/zmod/crt_properties.lean
index 37d22503fea43..3ad6fa9ef9866 100644
--- a/src/data/zmod/crt_properties.lean
+++ b/src/data/zmod/crt_properties.lean
@@ -24,7 +24,8 @@ lemma proj_fst' {m n : ℕ} (h : m.coprime n) (a : zmod m) (b : zmod n) :
     ((zmod.chinese_remainder h).symm (a,b)) = a :=
 begin
   change _ = prod.fst (a, b),
-  have h2 : zmod.cast_hom (show m.lcm n ∣ m * n, by simp [nat.lcm_dvd_iff]) (zmod m × zmod n) _ = _,
+  have h2 : zmod.cast_hom (show m.lcm n ∣ m * n,
+    by simp [nat.lcm_dvd_iff]) (zmod m × zmod n) _ = _,
     exact (zmod.chinese_remainder h).right_inv (a,b),
   conv_rhs { rw ←h2, },
   convert_to _ = (ring_hom.comp (ring_hom.fst (zmod m) (zmod n))
@@ -38,7 +39,8 @@ lemma proj_snd' {m n : ℕ} (h : m.coprime n) (a : zmod m) (b : zmod n) :
     ((zmod.chinese_remainder h).symm (a,b)) = b :=
 begin
   change _ = prod.snd (a, b),
-  have h2 : zmod.cast_hom (show m.lcm n ∣ m * n, by simp [nat.lcm_dvd_iff]) (zmod m × zmod n) _ = _,
+  have h2 : zmod.cast_hom (show m.lcm n ∣ m * n,
+    by simp [nat.lcm_dvd_iff]) (zmod m × zmod n) _ = _,
     exact (zmod.chinese_remainder h).right_inv (a,b),
   conv_rhs { rw ←h2, },
   convert_to _ = (ring_hom.comp (ring_hom.snd (zmod m) (zmod n))
@@ -78,11 +80,13 @@ lemma inv_snd {n : ℕ} (x : zmod (d * p^n)) (cop : d.coprime (p^n)) :
 
 variable (p)
 lemma proj_fst'' {n : ℕ} (hd : d.coprime p) (a : (zmod d)ˣ × (zmod (p^n))ˣ) :
-((zmod.chinese_remainder (nat.coprime.pow_right n hd)).inv_fun (↑(a.fst), ↑(a.snd)) : zmod d) = a.fst :=
+  ((zmod.chinese_remainder (nat.coprime.pow_right n hd)).inv_fun (↑(a.fst), ↑(a.snd)) : zmod d) =
+  a.fst :=
 by { rw ring_equiv.inv_fun_eq_symm, apply proj_fst', }
 
 lemma proj_snd'' [fact p.prime] {n : ℕ} (hd : d.coprime p) (a : (zmod d)ˣ × (zmod (p^n))ˣ) :
-(padic_int.to_zmod_pow n) ((zmod.chinese_remainder (nat.coprime.pow_right n hd)).inv_fun (↑(a.fst), ↑(a.snd)) : ℤ_[p]) = a.snd :=
+  (padic_int.to_zmod_pow n) ((zmod.chinese_remainder (nat.coprime.pow_right n hd)).inv_fun
+  (↑(a.fst), ↑(a.snd)) : ℤ_[p]) = a.snd :=
 begin
   rw [← zmod.int_cast_cast, map_int_cast, zmod.int_cast_cast, ring_equiv.inv_fun_eq_symm],
   convert proj_snd' _ _ _,
diff --git a/src/data/zmod/units.lean b/src/data/zmod/units.lean
index 825cec5193273..eefe95b8e93cc 100644
--- a/src/data/zmod/units.lean
+++ b/src/data/zmod/units.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ashvni Narayanan
 -/
 import data.zmod.basic
-import data.zmod.topology
+import topology.algebra.constructions
 
 /-!
 # Properties of units of ℤ/nℤ

From e594e8464a3a48da039ee10d6389553841bb0485 Mon Sep 17 00:00:00 2001
From: Ashvni <ashvni.n@gmail.com>
Date: Sat, 6 May 2023 10:26:25 +0100
Subject: [PATCH 4/9] removed references to implicit variables

---
 src/data/zmod/units.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/data/zmod/units.lean b/src/data/zmod/units.lean
index eefe95b8e93cc..d93568836ef7e 100644
--- a/src/data/zmod/units.lean
+++ b/src/data/zmod/units.lean
@@ -25,7 +25,7 @@ zmod, units
 open zmod nat
 namespace zmod
 /-- Same as `zmod.cast_hom_apply` with some hypotheses being made explicit. -/
-lemma cast_hom_apply' {n : ℕ} (R : Type*) [_inst_1 : ring R] {m : ℕ} [_inst_2 : char_p R m]
+lemma cast_hom_apply' {n : ℕ} (R : Type*) [ring R] {m : ℕ} [char_p R m]
   (h : m ∣ n) (i : zmod n) : (cast_hom h R) i = ↑i := cast_hom_apply i
 
 lemma coe_map_of_dvd {a b : ℕ} (h : a ∣ b) (x : units (zmod b)) :

From 3a3ee04d61ce44bbecd8e3761c009e20923ea9d9 Mon Sep 17 00:00:00 2001
From: Ashvni <ashvni.n@gmail.com>
Date: Sat, 6 May 2023 13:45:44 +0100
Subject: [PATCH 5/9] added namespace for crt lemmas

---
 src/data/zmod/crt_properties.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/data/zmod/crt_properties.lean b/src/data/zmod/crt_properties.lean
index 3ad6fa9ef9866..3a054fac64479 100644
--- a/src/data/zmod/crt_properties.lean
+++ b/src/data/zmod/crt_properties.lean
@@ -19,6 +19,9 @@ This file has some theorems regarding coercions with respect to the Chinese Rema
 zmod, CRT
 -/
 
+namespace zmod
+namespace chinese_remainder_theorem
+
 lemma proj_fst' {m n : ℕ} (h : m.coprime n) (a : zmod m) (b : zmod n) :
   zmod.cast_hom (show m ∣ m * n, from dvd.intro n rfl) (zmod m)
     ((zmod.chinese_remainder h).symm (a,b)) = a :=
@@ -91,3 +94,5 @@ begin
   rw [← zmod.int_cast_cast, map_int_cast, zmod.int_cast_cast, ring_equiv.inv_fun_eq_symm],
   convert proj_snd' _ _ _,
 end
+end chinese_remainder_theorem
+end zmod

From 0d2f77d343411d3a0aa8f06695f0adb2077e96f0 Mon Sep 17 00:00:00 2001
From: Ashvni <ashvni.n@gmail.com>
Date: Mon, 8 May 2023 11:58:32 +0100
Subject: [PATCH 6/9] suggested changes 1

---
 src/data/zmod/units.lean | 11 +++--------
 src/topology/maps.lean   |  2 +-
 2 files changed, 4 insertions(+), 9 deletions(-)

diff --git a/src/data/zmod/units.lean b/src/data/zmod/units.lean
index d93568836ef7e..113c593962fd6 100644
--- a/src/data/zmod/units.lean
+++ b/src/data/zmod/units.lean
@@ -28,13 +28,8 @@ namespace zmod
 lemma cast_hom_apply' {n : ℕ} (R : Type*) [ring R] {m : ℕ} [char_p R m]
   (h : m ∣ n) (i : zmod n) : (cast_hom h R) i = ↑i := cast_hom_apply i
 
-lemma coe_map_of_dvd {a b : ℕ} (h : a ∣ b) (x : units (zmod b)) :
-  is_unit (x : zmod a) :=
-begin
-  change is_unit ((x : zmod b) : zmod a),
-  rw [←zmod.cast_hom_apply' (zmod a) h (x : zmod b), ←ring_hom.coe_monoid_hom, ←units.coe_map],
-  apply units.is_unit,
-end
+lemma coe_map_of_dvd {a b : ℕ} (h : a ∣ b) {x : (zmod b)} (hx : is_unit x) :
+  is_unit (x : zmod a) := is_unit.map (cast_hom h (zmod a)).to_monoid_hom hx
 
 lemma is_unit_of_is_coprime_dvd {a b : ℕ} (h : a ∣ b) {x : ℕ} (hx : x.coprime b) :
   is_unit (x : zmod a) :=
@@ -43,7 +38,7 @@ begin
   { rw ←cast_nat_cast h x,
     { congr, },
     { refine zmod.char_p _, }, },
-  { apply coe_map_of_dvd h _, },
+  { apply coe_map_of_dvd h (units.is_unit _), },
 end
 
 lemma is_unit_mul {a b g : ℕ} (n : ℕ) (h1 : g.coprime a) (h2 : g.coprime b) :
diff --git a/src/topology/maps.lean b/src/topology/maps.lean
index 6e940dbb56137..03b19f249e025 100644
--- a/src/topology/maps.lean
+++ b/src/topology/maps.lean
@@ -226,7 +226,7 @@ namespace inducing
 lemma discrete_topology {X Y : Type*} [h1 : _root_.topological_space X]
   [h2 : _root_.topological_space Y] [discrete_topology Y] {f : X → Y} (inj : function.injective f)
   (ind : h1 = topological_space.induced f h2) : discrete_topology X :=
-embedding.discrete_topology (embedding.mk ⟨ind⟩ inj)
+(embedding.mk ⟨ind⟩ inj).discrete_topology
 end inducing
 
 /-- A function between topological spaces is a quotient map if it is surjective,

From 0f52ac63da1833666043275a3055ef2da9089386 Mon Sep 17 00:00:00 2001
From: Ashvni <ashvni.n@gmail.com>
Date: Mon, 8 May 2023 13:51:29 +0100
Subject: [PATCH 7/9] added discrete topology to mul_opposite

---
 src/topology/algebra/constructions.lean | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/src/topology/algebra/constructions.lean b/src/topology/algebra/constructions.lean
index 73c46ac1efe15..c26392afd5562 100644
--- a/src/topology/algebra/constructions.lean
+++ b/src/topology/algebra/constructions.lean
@@ -143,12 +143,10 @@ begin
   { apply_instance, },
 end
 
+instance {M : Type*} [topological_space M] [discrete_topology M] : discrete_topology Mᵐᵒᵖ :=
+inducing.discrete_topology mul_opposite.unop_injective rfl
+
 lemma discrete_prod_units {X Y : Type*} [monoid X] [monoid Y] [topological_space X]
   [discrete_topology X] [topological_space Y] [discrete_topology Y] : discrete_topology (X × Y)ˣ :=
-begin
-  apply @embedding.discrete_topology _ _ _ _ prod.discrete_topology (units.embed_product _)
-    (units.embedding_embed_product),
-  { apply_instance, },
-  { refine inducing.discrete_topology (mul_opposite.unop_injective) rfl, },
-end
+embedding.discrete_topology (units.embedding_embed_product)
 end units

From 4a0e970ace6f07a5fbfc3d16f5b34d1606113898 Mon Sep 17 00:00:00 2001
From: Ashvni <ashvni.n@gmail.com>
Date: Mon, 8 May 2023 16:30:47 +0100
Subject: [PATCH 8/9] adding additive structure to instance

---
 src/topology/algebra/constructions.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/topology/algebra/constructions.lean b/src/topology/algebra/constructions.lean
index c26392afd5562..672c42e173f57 100644
--- a/src/topology/algebra/constructions.lean
+++ b/src/topology/algebra/constructions.lean
@@ -143,6 +143,7 @@ begin
   { apply_instance, },
 end
 
+@[to_additive]
 instance {M : Type*} [topological_space M] [discrete_topology M] : discrete_topology Mᵐᵒᵖ :=
 inducing.discrete_topology mul_opposite.unop_injective rfl
 

From 6281a669f587d6532fbac53137cdd7394d5c7620 Mon Sep 17 00:00:00 2001
From: Ashvni <ashvni.n@gmail.com>
Date: Mon, 8 May 2023 18:44:20 +0100
Subject: [PATCH 9/9] suggested changes 2

---
 src/topology/algebra/constructions.lean | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/topology/algebra/constructions.lean b/src/topology/algebra/constructions.lean
index 672c42e173f57..7d769df2dd2b8 100644
--- a/src/topology/algebra/constructions.lean
+++ b/src/topology/algebra/constructions.lean
@@ -63,6 +63,9 @@ op_homeomorph.comap_nhds_eq x
 @[simp, to_additive] lemma comap_unop_nhds (x : M) : comap (unop : Mᵐᵒᵖ → M) (𝓝 x) = 𝓝 (op x) :=
 op_homeomorph.symm.comap_nhds_eq x
 
+@[to_additive]
+instance {M : Type*} [topological_space M] [discrete_topology M] : discrete_topology Mᵐᵒᵖ :=
+inducing.discrete_topology mul_opposite.unop_injective rfl
 end mul_opposite
 
 namespace units
@@ -116,7 +119,9 @@ by simp only [inducing_embed_product.continuous_iff, embed_product_apply, (∘),
 (units.continuous_iff.1 continuous_id).2
 
 /-- The inverse map `units.inv` is continuous with respect to the topology induced by
-  `units.coe_hom` on units. -/
+  `units.coe_hom` on units.
+
+  Note this is not the topology used by default in mathlib.-/
 @[continuity]
 lemma induced_top_cont_inv {X : Type*} [topological_space X] [discrete_topology X] [monoid X] :
   @continuous _ _ (topological_space.induced (units.coe_hom X) infer_instance) _
@@ -143,10 +148,6 @@ begin
   { apply_instance, },
 end
 
-@[to_additive]
-instance {M : Type*} [topological_space M] [discrete_topology M] : discrete_topology Mᵐᵒᵖ :=
-inducing.discrete_topology mul_opposite.unop_injective rfl
-
 lemma discrete_prod_units {X Y : Type*} [monoid X] [monoid Y] [topological_space X]
   [discrete_topology X] [topological_space Y] [discrete_topology Y] : discrete_topology (X × Y)ˣ :=
 embedding.discrete_topology (units.embedding_embed_product)