Skip to content

Implemented StandardModel.gaugeGroupℤ₃SubGroup and StandardModel.GaugeGroupℤ₃#1179

Merged
jstoobysmith merged 2 commits into
leanprover-community:masterfrom
kastch:feat/6V2GV-6V2G3
Jun 12, 2026
Merged

Implemented StandardModel.gaugeGroupℤ₃SubGroup and StandardModel.GaugeGroupℤ₃#1179
jstoobysmith merged 2 commits into
leanprover-community:masterfrom
kastch:feat/6V2GV-6V2G3

Conversation

@kastch

@kastch kastch commented Jun 12, 2026

Copy link
Copy Markdown
Contributor

Implemented StandardModel.gaugeGroupℤ₃SubGroup and StandardModel.GaugeGroupℤ₃
Closing tags 6V2GV and 6V2G3

Added the inclusion of third roots of unity into sixth roots of unity, the induced homomorphism into GaugeGroupI, centrality/normality API for the subgroup, and the quotient map GaugeGroupℤ₃.mk.

@github-actions

Copy link
Copy Markdown
Contributor

Thank you for this PR, which will now be reviewed. Please
see our review guidelines
if you are not familiar with the process. You should expect a back and forth
with a reviewer before your PR is merged. See also that link for how to
add appropriate labels to your PR. The PR will also go through a number
of automated checks. You can learn more about these here,
including how to run them locally.

If you want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

@kastch kastch changed the title Implemented StandardModel.gaugeGroupℤ₃SubGroup and StandardModel.Gaug… Implemented StandardModel.gaugeGroupℤ₃SubGroup and StandardModel.GaugeGroupℤ₃ Jun 12, 2026
Comment thread Physlib/Particles/StandardModel/Basic.lean

@jstoobysmith jstoobysmith left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Approved - many thanks. Will merge when passes linters

@jstoobysmith jstoobysmith added ready-to-merge This PR is approved and will be merged shortly t-particles Particles labels Jun 12, 2026
@jstoobysmith jstoobysmith merged commit ede623d into leanprover-community:master Jun 12, 2026
6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR is approved and will be merged shortly t-particles Particles

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants