ScopedRingNotation

Scoped operations for abstract rings and maps between rings

Open in Workbench View on GitHub

1-- Scoped operations for abstract rings and maps between rings.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module ScopedRingNotation8import Grace.Cumulus.Algebra.Ring910section Rings11variable (A add zero neg mul one : Set)12hypothesis source : IsCommRing(A, add, zero, neg, mul, one)13notation ring R := (A, add, zero, neg, mul, one)1415theorem simplify (x y : Set)16  requires hx : x ∈ A17  requires hy : y ∈ A18  shows (x + y) * 1 - y + 0 = x19proof20  ring2122section Maps23variable (f B plus z minus times unit : Set)24hypothesis target : IsCommRing(B, plus, z, minus, times, unit)25hypothesis hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)26notation ring S := (B, plus, z, minus, times, unit)2728theorem preserves_sum (x y : Set)29  requires hx : x ∈ A30  requires hy : y ∈ A31  shows f(x + y) = f(x) + f(y)32proof33  exact IsRingHom.add with hom, hx, hy3435theorem explicit_scopes (x y : Set)36  requires hx : x ∈ A37  requires hy : y ∈ A38  shows f(R[x * y]) = S[f(x) * f(y)]39proof40  exact IsRingHom.mul with hom, hx, hy4142theorem preserves_one43  shows f(R[1]) = S[1]44proof45  exact IsRingHom.one with hom46end Maps4748-- Ending Maps restores the single-ring notation context.49theorem restored (x : Set)50  requires hx : x ∈ A51  shows -x + x = 052proof53  ring54end Rings55