Skip to content

Conversation

@Alizter
Copy link
Collaborator

@Alizter Alizter commented Jan 4, 2025

This isn't true definitionally due to the way we define subgroups. This lemma at least lets us pass along the obvious equivalence when it appears in arguments.

Relies on (because of Require)

@Alizter Alizter marked this pull request as draft January 4, 2025 02:11
@Alizter Alizter requested a review from jdchristensen January 4, 2025 19:22
@Alizter Alizter marked this pull request as ready for review January 4, 2025 19:22
Signed-off-by: Ali Caglayan <[email protected]>

<!-- ps-id: d6d33e40-310f-4066-bb9d-34775e41cbbd -->
Signed-off-by: Ali Caglayan <[email protected]>
@Alizter Alizter force-pushed the ps/rr/sugroup_group_of_maximal_subgroup_is_iso_to_original_group branch from 55276e2 to 3b5d305 Compare January 7, 2025 12:46
@Alizter Alizter merged commit 12bd284 into HoTT:master Jan 8, 2025
22 checks passed
@Alizter Alizter deleted the ps/rr/sugroup_group_of_maximal_subgroup_is_iso_to_original_group branch January 8, 2025 09:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants