BundledRings

Bundled rings: a section over a commutative ring structure, its notation

Open in Workbench View on GitHub

1-- Bundled rings: a section over a commutative ring structure, its notation2-- read off the hypothesis, and the integers as a bundled value.3-- 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 BundledRings9import Grace.Cumulus.Algebra.Ring10import Grace.Cumulus.Int.Ring1112-- Under the hypothesis CommRing(R) a binder (x : R) is x ∈ R.carrier, the13-- operations are x + y, x * y, and -x, and R[0], R[1], R[2] are the ring's14-- own constants and numerals; `ring` reads the operation graphs off R.15section Rings16variable (R : Set)17hypothesis ring : CommRing(R)1819theorem square_sum (x y : R)20  shows (x + y) * (x + y) = x * x + R[2] * (x * y) + y * y21proof22  ring2324theorem neg_cancel (x y : R)25  shows -x + x + y * R[1] + R[0] = y26proof27  ring2829theorem closed (x y : R)30  shows (x + y) * -x ∈ R.carrier31proof32  typecheck3334theorem mul_comm (x y : R)35  shows x * y = y * x36proof37  have comm := CommRing.parts with ring38  exact IsCommRing.mul_comm with comm, *39end Rings4041-- The integers as a bundled ring: the structure value over the existing42-- instance, and the section theorem instantiated at it.43def integerRing : Set := Ring.mk(ℤ, integerAdd, integerZero, integerNeg, integerMul, integerOne)4445instance integerRing.comm_ring46  shows CommRing(integerRing)47proof48  unfold integerRing49  exact CommRing.of_parts with integers.comm_ring5051theorem square_sum.integers (x y : Set)52  requires xIn : x ∈ integerRing.carrier53  requires yIn : y ∈ integerRing.carrier54  shows (x + y) * (x + y) = x * x + integerRing[2] * (x * y) + y * y55proof56  exact square_sum with *57