GeneratedSubrings

Generated subrings with scoped structure notation

Open in Workbench View on GitHub

1-- Generated subrings with scoped structure notation.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module GeneratedSubrings8import Grace.Cumulus.Algebra.Ring.GeneratedSubring910section Generation11variable (A add zero neg mul one : Set)12notation ring R := (A, add, zero, neg, mul, one)13hypothesis ring : IsCommRing(R)1415theorem generated_elements_stay_in_subring (G S : Set)16  requires subring : IsSubring(R, S)17  requires generators : G ⊆ S18  shows generatedSubring(R, G) ⊆ S19proof20  exact generatedSubring.least at A, add, zero, neg, mul, one, G, S with *2122theorem generating_twice_changes_nothing (G : Set)23  shows generatedSubring(R, generatedSubring(R, G)) = generatedSubring(R, G)24proof25  exact generatedSubring.idempotent at A, add, zero, neg, mul, one, G with *2627theorem a_subring_generates_itself (S : Set)28  requires subring : IsSubring(R, S)29  shows generatedSubring(R, S) = S30proof31  exact generatedSubring.eq_of_subring at A, add, zero, neg, mul, one, S with *3233end Generation34