Ideal_of_Unit_is_Whole_Ring
Provedidealsproofwikiringsunits
Let R be a ring with unity. Let J be an ideal. If J contains a unit, then J = R.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Ideal_of_Unit_is_Whole_Ring {R : Type _} [CommRing R] (J : Ideal R) (u : R) (hu : IsUnit u) (huJ : u ∈ J) : J = ⊤ := by sorrySource