Subdomain_Test

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

integral-domainsproofwikisubrings

The unity of the ring belongs to any subring.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Subdomain_Test {R : Type _} [CommRing R] [IsDomain R] (S : Subring R) : (1 : R) ∈ S := by sorry

Source