Skip to content

Add orbit_representatives_and_stabilizers for 0-dim. subspaces#4465

Merged
simonbrandhorst merged 1 commit intooscar-system:masterfrom
ThomasBreuer:TB_orbit_triv_space
Jan 15, 2025
Merged

Add orbit_representatives_and_stabilizers for 0-dim. subspaces#4465
simonbrandhorst merged 1 commit intooscar-system:masterfrom
ThomasBreuer:TB_orbit_triv_space

Conversation

@ThomasBreuer
Copy link
Copy Markdown
Member

as promised in a comment for #4464

@simonbrandhorst simonbrandhorst enabled auto-merge (squash) January 15, 2025 09:08
@simonbrandhorst simonbrandhorst merged commit 34f980c into oscar-system:master Jan 15, 2025
@codecov
Copy link
Copy Markdown

codecov Bot commented Jan 15, 2025

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 84.40%. Comparing base (e993383) to head (c79b3bf).
Report is 138 commits behind head on master.

Additional details and impacted files
@@            Coverage Diff             @@
##           master    #4465      +/-   ##
==========================================
- Coverage   84.41%   84.40%   -0.01%     
==========================================
  Files         668      668              
  Lines       88591    88592       +1     
==========================================
  Hits        74780    74780              
- Misses      13811    13812       +1     
Files with missing lines Coverage Δ
src/Groups/gsets.jl 92.61% <100.00%> (+0.02%) ⬆️

... and 1 file with indirect coverage changes

@ThomasBreuer ThomasBreuer deleted the TB_orbit_triv_space branch January 15, 2025 10:20
@aaruni96 aaruni96 added package: GAP release notes: to be added PRs introducing changes that should be (but have not yet been) mentioned in the release notes labels Jan 30, 2025
@fingolfin fingolfin changed the title orbit_representatives_and_stabilizers for 0-dim. subspaces Add orbit_representatives_and_stabilizers for 0-dim. subspaces Feb 27, 2025
@fingolfin fingolfin added enhancement New feature or request release notes: use title For PRs: the title of this PR is suitable for direct use in the release notes and removed package: GAP release notes: to be added PRs introducing changes that should be (but have not yet been) mentioned in the release notes labels Feb 27, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement New feature or request release notes: use title For PRs: the title of this PR is suitable for direct use in the release notes topic: groups

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants