feat(Topology/Algebra/Ring/Ideal): the connected component of zero is an ideal (leanprover-community#35403)

This PR defines the connected component of zero as an ideal.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/Topology/Algebra/Ring/Ideal.lean

@@ -45,6 +45,20 @@ https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234852.
 theorem Ideal.closure_eq_of_isClosed (I : Ideal R) (hI : IsClosed (I : Set R)) : I.closure = I :=
   SetLike.ext' hI.closure_eq
 
+variable (R)
+
+/-- The connected component of zero in a topological ring as an ideal. -/
+def Ideal.connectedComponentOfZero : Ideal R where
+  __ := AddSubgroup.connectedComponentOfZero R
+  smul_mem' c x h := IsConnected.subset_connectedComponent
+    (isConnected_connectedComponent.image _ (continuous_const_mul c).continuousOn)
+    ⟨0, mem_connectedComponent, mul_zero c⟩ ⟨x, h, rfl⟩
+
+@[simp]
+theorem Ideal.coe_connectedComponentOfZero :
+    (Ideal.connectedComponentOfZero R : Set R) = connectedComponent 0 :=
+  rfl
+
 end Ring
 
 section CommRing