Grace/Cumulus/Real/Field.g17

Open in Workbench Download source

Imports

Inverse · Algebra.Ring.Basic

Declarations

• realRing def
• realRing.carrierOf theorem derivation
• realRing.comm_ring instance derivation
• realRing.field instance derivation

Source

1-- The real numbers as one bundled structure: the ring value realRing of2-- the Dedekind reals, a commutative ring and a field3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Real.Field9import Inverse10import Algebra.Ring.Basic1112-- The bundled real ring: the carrier ℝ with its addition, zero, negation,13-- multiplication, and one.14def realRing : Set := Ring.mk(ℝ, realAdd, realZero, realNeg, realMul, realOne)1516theorem realRing.carrierOf17  shows Ring.carrier(realRing) = ℝ18proof19  simp [realRing, Ring.mk.carrier]2021instance realRing.comm_ring22  shows CommRing(realRing)23proof24  have parts := reals.comm_ring25  unfold realRing26  exact CommRing.of_parts with parts2728instance realRing.field29  shows Field(realRing)30proof31  have parts := reals.field32  unfold realRing33  exact Field.of_inverse with parts34