feat(number_theory/number_field/basic) : the ring of integers of a nu…

…mber field is not a field (#11956)

src/data/int/char_zero.lean

@@ -36,3 +36,7 @@ theorem cast_ne_zero [add_group α] [has_one α] [char_zero α] {n : ℤ} : (n :
 not_congr cast_eq_zero
 
 end int
+
+lemma ring_hom.injective_int {α : Type*} [ring α] (f : ℤ →+* α) [char_zero α] :
+  function.injective f :=
+subsingleton.elim (int.cast_ring_hom _) f ▸ int.cast_injective

src/number_theory/number_field.lean

@@ -43,6 +43,19 @@ class number_field (K : Type*) [field K] : Prop :=
 open function
 open_locale classical big_operators
 
+/-- `ℤ` with its usual ring structure is not a field. -/
+lemma int.not_is_field : ¬ is_field ℤ :=
+begin
+  intro hf,
+  cases hf.mul_inv_cancel two_ne_zero with inv2 hinv2,
+  have not_even_2 : ¬ even (2 : ℤ),
+  { rw ← int.odd_iff_not_even,
+    apply int.odd.of_mul_left,
+    rw [hinv2, int.odd_iff_not_even],
+    exact int.not_even_one, },
+  exact not_even_2 (even_bit0 1),
+end
+
 namespace number_field
 
 variables (K L : Type*) [field K] [field L] [nf : number_field K]
@@ -96,6 +109,16 @@ variables (K)
 
 instance [number_field K] : char_zero (𝓞 K) := char_zero.of_module _ K
 
+/-- The ring of integers of a number field is not a field. -/
+lemma not_is_field [number_field K] : ¬ is_field (𝓞 K) :=
+begin
+  have h_inj : function.injective ⇑(algebra_map ℤ (𝓞 K)),
+  { exact ring_hom.injective_int (algebra_map ℤ (𝓞 K)) },
+  intro hf,
+  exact int.not_is_field ((is_integral.is_field_iff_is_field
+    (is_integral_closure.is_integral_algebra ℤ K) h_inj).mpr hf)
+end
+
 instance [number_field K] : is_dedekind_domain (𝓞 K) :=
 is_integral_closure.is_dedekind_domain ℤ ℚ K _