[GOAL]
x : { x // x ∈ 𝓞 ℚ }
⊢ IsUnit x ↔ ↑x = 1 ∨ ↑x = -1
[PROOFSTEP]
simp_rw [(isUnit_map_iff (Rat.ringOfIntegersEquiv : 𝓞 ℚ →+* ℤ) x).symm, Int.isUnit_iff, RingEquiv.coe_toRingHom,
  RingEquiv.map_eq_one_iff, RingEquiv.map_eq_neg_one_iff, ← Subtype.coe_injective.eq_iff]
[GOAL]
x : { x // x ∈ 𝓞 ℚ }
⊢ ↑x = ↑1 ∨ ↑x = ↑(-1) ↔ ↑x = 1 ∨ ↑x = -1
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : { x // x ∈ 𝓞 K }
⊢ IsUnit x ↔ |↑(↑(RingOfIntegers.norm ℚ) x)| = 1
[PROOFSTEP]
convert (RingOfIntegers.isUnit_norm ℚ (F := K)).symm
[GOAL]
case h.e'_2.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : { x // x ∈ 𝓞 K }
⊢ |↑(↑(RingOfIntegers.norm ℚ) x)| = 1 ↔ IsUnit (↑(RingOfIntegers.norm ℚ) x)
[PROOFSTEP]
rw [← abs_one, abs_eq_abs, ← Rat.RingOfIntegers.isUnit_iff]
[GOAL]
K : Type u_1
inst✝ : Field K
x✝¹ x✝ : { x // x ∈ 𝓞 K }ˣ
h : (fun x => ↑↑x) x✝¹ = (fun x => ↑↑x) x✝
⊢ x✝¹ = x✝
[PROOFSTEP]
rwa [SetLike.coe_eq_coe, Units.eq_iff] at h 
[GOAL]
K : Type u_1
inst✝ : Field K
x : { x // x ∈ 𝓞 K }ˣ
n : ℕ
⊢ ↑↑(x ^ n) = ↑↑x ^ n
[PROOFSTEP]
rw [← SubmonoidClass.coe_pow, ← val_pow_eq_pow_val]
[GOAL]
K : Type u_1
inst✝ : Field K
x : { x // x ∈ 𝓞 K }ˣ
n : ℤ
⊢ ↑↑(x ^ n) = ↑↑x ^ n
[PROOFSTEP]
change ((Units.coeHom K).comp (map (algebraMap (𝓞 K) K))) (x ^ n) = _
[GOAL]
K : Type u_1
inst✝ : Field K
x : { x // x ∈ 𝓞 K }ˣ
n : ℤ
⊢ ↑(MonoidHom.comp (coeHom K) (map ↑(algebraMap { x // x ∈ 𝓞 K } K))) (x ^ n) = ↑↑x ^ n
[PROOFSTEP]
exact map_zpow _ x n
[GOAL]
K : Type u_1
inst✝¹ : Field K
x : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
⊢ x ∈ torsion K ↔ ∀ (w : InfinitePlace K), ↑w ↑↑x = 1
[PROOFSTEP]
rw [eq_iff_eq (x : K) 1, torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
[GOAL]
K : Type u_1
inst✝¹ : Field K
x : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
⊢ (∃ n, 0 < n ∧ x ^ n = 1) ↔ ∀ (φ : K →+* ℂ), ‖↑φ ↑↑x‖ = 1
[PROOFSTEP]
refine ⟨fun ⟨n, h_pos, h_eq⟩ φ => ?_, fun h => ?_⟩
[GOAL]
case refine_1
K : Type u_1
inst✝¹ : Field K
x : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
x✝ : ∃ n, 0 < n ∧ x ^ n = 1
φ : K →+* ℂ
n : ℕ
h_pos : 0 < n
h_eq : x ^ n = 1
⊢ ‖↑φ ↑↑x‖ = 1
[PROOFSTEP]
refine norm_map_one_of_pow_eq_one φ.toMonoidHom (k := ⟨n, h_pos⟩) ?_
[GOAL]
case refine_1
K : Type u_1
inst✝¹ : Field K
x : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
x✝ : ∃ n, 0 < n ∧ x ^ n = 1
φ : K →+* ℂ
n : ℕ
h_pos : 0 < n
h_eq : x ^ n = 1
⊢ ↑↑x ^ ↑{ val := n, property := h_pos } = 1
[PROOFSTEP]
rw [PNat.mk_coe, ← coe_pow, h_eq, coe_one]
[GOAL]
case refine_2
K : Type u_1
inst✝¹ : Field K
x : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
h : ∀ (φ : K →+* ℂ), ‖↑φ ↑↑x‖ = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
obtain ⟨n, hn, hx⟩ := Embeddings.pow_eq_one_of_norm_eq_one K ℂ x.val.prop h
[GOAL]
case refine_2.intro.intro
K : Type u_1
inst✝¹ : Field K
x : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
h : ∀ (φ : K →+* ℂ), ‖↑φ ↑↑x‖ = 1
n : ℕ
hn : 0 < n
hx : ↑↑x ^ n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
exact ⟨n, hn, by ext; rw [coe_pow, hx, coe_one]⟩
[GOAL]
K : Type u_1
inst✝¹ : Field K
x : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
h : ∀ (φ : K →+* ℂ), ‖↑φ ↑↑x‖ = 1
n : ℕ
hn : 0 < n
hx : ↑↑x ^ n = 1
⊢ x ^ n = 1
[PROOFSTEP]
ext
[GOAL]
case a.a
K : Type u_1
inst✝¹ : Field K
x : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
h : ∀ (φ : K →+* ℂ), ‖↑φ ↑↑x‖ = 1
n : ℕ
hn : 0 < n
hx : ↑↑x ^ n = 1
⊢ ↑↑(x ^ n) = ↑↑1
[PROOFSTEP]
rw [coe_pow, hx, coe_one]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype { x // x ∈ torsion K }
[PROOFSTEP]
refine @Fintype.ofFinite _ (Set.finite_coe_iff.mpr ?_)
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Set.Finite ↑(torsion K)
[PROOFSTEP]
refine Set.Finite.of_finite_image ?_ ((coe_injective K).injOn _)
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Set.Finite ((fun x => ↑↑x) '' ↑(torsion K))
[PROOFSTEP]
refine (Embeddings.finite_of_norm_le K ℂ 1).subset (fun a ⟨u, ⟨h_tors, h_ua⟩⟩ => ⟨?_, fun φ => ?_⟩)
[GOAL]
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x => ↑↑x) '' ↑(torsion K)
u : { x // x ∈ 𝓞 K }ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x => ↑↑x) u = a
⊢ IsIntegral ℤ a
[PROOFSTEP]
rw [← h_ua]
[GOAL]
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x => ↑↑x) '' ↑(torsion K)
u : { x // x ∈ 𝓞 K }ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x => ↑↑x) u = a
⊢ IsIntegral ℤ ((fun x => ↑↑x) u)
[PROOFSTEP]
exact u.val.prop
[GOAL]
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x => ↑↑x) '' ↑(torsion K)
u : { x // x ∈ 𝓞 K }ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x => ↑↑x) u = a
φ : K →+* ℂ
⊢ ‖↑φ a‖ ≤ 1
[PROOFSTEP]
rw [← h_ua]
[GOAL]
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x => ↑↑x) '' ↑(torsion K)
u : { x // x ∈ 𝓞 K }ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x => ↑↑x) u = a
φ : K →+* ℂ
⊢ ‖↑φ ((fun x => ↑↑x) u)‖ ≤ 1
[PROOFSTEP]
exact
  le_of_eq
    ((eq_iff_eq _ 1).mp ((mem_torsion K).mp h_tors) φ)
      -- a shortcut instance to stop the next instance from timing out
[GOAL]
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
⊢ ζ ∈ rootsOfUnity k { x // x ∈ 𝓞 K } ↔ ζ = 1
[PROOFSTEP]
rw [mem_rootsOfUnity]
[GOAL]
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
⊢ ζ ^ ↑k = 1 ↔ ζ = 1
[PROOFSTEP]
refine ⟨fun h => ?_, fun h => by rw [h, one_pow]⟩
[GOAL]
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
h : ζ = 1
⊢ ζ ^ ↑k = 1
[PROOFSTEP]
rw [h, one_pow]
[GOAL]
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
h : ζ ^ ↑k = 1
⊢ ζ = 1
[PROOFSTEP]
refine orderOf_eq_one_iff.mp (Nat.eq_one_of_dvd_coprimes hc ?_ ?_)
[GOAL]
case refine_1
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
h : ζ ^ ↑k = 1
⊢ orderOf ζ ∣ ↑k
[PROOFSTEP]
exact orderOf_dvd_of_pow_eq_one h
[GOAL]
case refine_2
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
h : ζ ^ ↑k = 1
⊢ orderOf ζ ∣ ↑(torsion_order K)
[PROOFSTEP]
have hζ : ζ ∈ torsion K := by
  rw [torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
  exact ⟨k, k.prop, h⟩
[GOAL]
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
h : ζ ^ ↑k = 1
⊢ ζ ∈ torsion K
[PROOFSTEP]
rw [torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
[GOAL]
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
h : ζ ^ ↑k = 1
⊢ ∃ n, 0 < n ∧ ζ ^ n = 1
[PROOFSTEP]
exact ⟨k, k.prop, h⟩
[GOAL]
case refine_2
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
h : ζ ^ ↑k = 1
hζ : ζ ∈ torsion K
⊢ orderOf ζ ∣ ↑(torsion_order K)
[PROOFSTEP]
rw [orderOf_submonoid (⟨ζ, hζ⟩ : torsion K)]
[GOAL]
case refine_2
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
h : ζ ^ ↑k = 1
hζ : ζ ∈ torsion K
⊢ orderOf { val := ζ, property := hζ } ∣ ↑(torsion_order K)
[PROOFSTEP]
exact orderOf_dvd_card_univ
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ rootsOfUnity (torsion_order K) { x // x ∈ 𝓞 K } = torsion K
[PROOFSTEP]
ext ζ
[GOAL]
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : { x // x ∈ 𝓞 K }ˣ
⊢ ζ ∈ rootsOfUnity (torsion_order K) { x // x ∈ 𝓞 K } ↔ ζ ∈ torsion K
[PROOFSTEP]
rw [torsion, mem_rootsOfUnity]
[GOAL]
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : { x // x ∈ 𝓞 K }ˣ
⊢ ζ ^ ↑(torsion_order K) = 1 ↔ ζ ∈ CommGroup.torsion { x // x ∈ 𝓞 K }ˣ
[PROOFSTEP]
refine ⟨fun h => ?_, fun h => ?_⟩
[GOAL]
case h.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : { x // x ∈ 𝓞 K }ˣ
h : ζ ^ ↑(torsion_order K) = 1
⊢ ζ ∈ CommGroup.torsion { x // x ∈ 𝓞 K }ˣ
[PROOFSTEP]
rw [CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
[GOAL]
case h.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : { x // x ∈ 𝓞 K }ˣ
h : ζ ^ ↑(torsion_order K) = 1
⊢ ∃ n, 0 < n ∧ ζ ^ n = 1
[PROOFSTEP]
exact ⟨↑(torsion_order K), (torsion_order K).prop, h⟩
[GOAL]
case h.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : { x // x ∈ 𝓞 K }ˣ
h : ζ ∈ CommGroup.torsion { x // x ∈ 𝓞 K }ˣ
⊢ ζ ^ ↑(torsion_order K) = 1
[PROOFSTEP]
exact Subtype.ext_iff.mp (@pow_card_eq_one (torsion K) _ ⟨ζ, h⟩ _)
