feat(RingTheory/Ideal): 37 cast to an ideal is just the whole ring. (#20244)

https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/IdemSemiring.20.2B.20OfNat

Author: Julian

Mathlib/Algebra/Order/Kleene.lean

@@ -133,6 +133,14 @@ scoped[Computability] attribute [simp] add_eq_sup
 
 theorem add_idem (a : α) : a + a = a := by simp
 
+lemma natCast_eq_one {n : ℕ} (nezero : n ≠ 0) : (n : α) = 1 := by
+  induction n, Nat.one_le_iff_ne_zero.mpr nezero using Nat.le_induction with
+  | base => exact Nat.cast_one
+  | succ x _ hx => rw [Nat.cast_add, hx, Nat.cast_one, add_idem 1]
+
+lemma ofNat_eq_one {n : ℕ} [n.AtLeastTwo] : (ofNat(n) : α) = 1 :=
+  natCast_eq_one <| Nat.not_eq_zero_of_lt Nat.AtLeastTwo.prop
+
 theorem nsmul_eq_self : ∀ {n : ℕ} (_ : n ≠ 0) (a : α), n • a = a
   | 0, h => (h rfl).elim
   | 1, _ => one_nsmul

Mathlib/RingTheory/Ideal/Operations.lean

@@ -851,6 +851,14 @@ variable (R) in
 theorem top_pow (n : ℕ) : (⊤ ^ n : Ideal R) = ⊤ :=
   Nat.recOn n one_eq_top fun n ih => by rw [pow_succ, ih, top_mul]
 
+theorem natCast_eq_top {n : ℕ} (hn : n ≠ 0) : (n : Ideal R) = ⊤ :=
+  natCast_eq_one hn |>.trans one_eq_top
+
+/-- `3 : Ideal R` is *not* the ideal generated by 3 (which would be spelt
+    `Ideal.span {3}`), it is simply `1 + 1 + 1 = ⊤`. -/
+theorem ofNat_eq_top {n : ℕ} [n.AtLeastTwo] : (ofNat(n) : Ideal R) = ⊤ :=
+  ofNat_eq_one.trans one_eq_top
+
 variable (I)
 
 lemma radical_pow : ∀ {n}, n ≠ 0 → radical (I ^ n) = radical I