Skip to content

[Merged by Bors] - feat(Topology/Group): Open normal subgroup#16980

Closed
Thmoas-Guan wants to merge 5 commits intomasterfrom
open-normal-subgroup
Closed

[Merged by Bors] - feat(Topology/Group): Open normal subgroup#16980
Thmoas-Guan wants to merge 5 commits intomasterfrom
open-normal-subgroup

Conversation

@Thmoas-Guan
Copy link
Copy Markdown
Collaborator

@Thmoas-Guan Thmoas-Guan commented Sep 20, 2024

Define the type of open normal subgroup in a topological group.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 20, 2024 •
edited
Loading

PR summary 5354f595f1

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ OpenNormalAddSubgroup
+ OpenNormalSubgroup
+ instInfOpenNormalSubgroup
+ instPartialOrderOpenNormalSubgroup
+ instSemilatticeInfOpenNormalSubgroup
+ instSemilatticeSupOpenNormalSubgroup
+ instance (H : OpenNormalSubgroup G) : H.toSubgroup.Normal := H.isNormal'
+ instance : Coe (OpenNormalSubgroup G) (Subgroup G)
+ instance : SetLike (OpenNormalSubgroup G) G
+ instance : SubgroupClass (OpenNormalSubgroup G) G
+ instance [ContinuousMul G] : Lattice (OpenNormalSubgroup G)
+ instance [ContinuousMul G] : Sup (OpenNormalSubgroup G)
+ toSubgroup_injective

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

This was referenced Sep 20, 2024
Closed
Closed
@Thmoas-Guan Thmoas-Guan added t-topology Topological spaces, uniform spaces, metric spaces, filters t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress labels Sep 23, 2024
jcommelin
jcommelin reviewed Sep 27, 2024
View reviewed changes
@Thmoas-Guan Thmoas-Guan removed the WIP Work in progress label Sep 29, 2024
jcommelin
jcommelin reviewed Oct 4, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Oct 4, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 4, 2024
@Thmoas-Guan
feat(Topology/Group): Open normal subgroup (#16980)
8834646 
Define the type of open normal subgroup in a topological group.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 4, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Topology/Group): Open normal subgroup [Merged by Bors] - feat(Topology/Group): Open normal subgroup Oct 4, 2024
@mathlib-bors mathlib-bors bot closed this Oct 4, 2024
@mathlib-bors mathlib-bors bot deleted the open-normal-subgroup branch October 4, 2024 11:14
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@Thmoas-Guan @jcommelin