-- The real numbers as one bundled structure: the ring value realRing of
-- the Dedekind reals, a commutative ring and a field
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Real.Field
import Inverse
import Algebra.Ring.Basic

-- The bundled real ring: the carrier ℝ with its addition, zero, negation,
-- multiplication, and one.
def realRing : Set := Ring.mk(ℝ, realAdd, realZero, realNeg, realMul, realOne)

theorem realRing.carrierOf
  shows Ring.carrier(realRing) = ℝ
proof
  simp [realRing, Ring.mk.carrier]

instance realRing.comm_ring
  shows CommRing(realRing)
proof
  have parts := reals.comm_ring
  unfold realRing
  exact CommRing.of_parts with parts

instance realRing.field
  shows Field(realRing)
proof
  have parts := reals.field
  unfold realRing
  exact Field.of_inverse with parts