Unity_is_Unit
Provedproofwikiringsunits
The unity in a ring is a unit.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Unity_is_Unit {R : Type _} [Ring R] : IsUnit (1 : R) := by sorrySource
The unity in a ring is a unit.
import Mathlib.Analysis.Complex.Basic
theorem Unity_is_Unit {R : Type _} [Ring R] : IsUnit (1 : R) := by sorry