Skip to content

chore(SpecificGroups/Alternating/Simple): remove a convert#39201

Open
b-mehta wants to merge 1 commit into
leanprover-community:masterfrom
b-mehta:alternating-simple-convert
Open

chore(SpecificGroups/Alternating/Simple): remove a convert#39201
b-mehta wants to merge 1 commit into
leanprover-community:masterfrom
b-mehta:alternating-simple-convert

Conversation

@b-mehta
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta commented May 11, 2026

As mentioned here https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/support.20of.20permutations.20on.20Type.20instead.20of.20Fintype/with/593547821

I misdiagnosed the issue in that thread, and this PR only fixes one of the issues.
The "issue" in this case was that the lemma cycleType_ofSubtype contains a non-variable instance of Fintype (Subtype p), which means that when applying the lemma, the "wrong" instance could be picked. The correct pattern is that if a lemma requires Fintype _, then it should be stated explicitly in the type, even if that instance is derivable from other hypotheses. (An existing example is https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Fintype/Sets.html#Set.toFinset_union).


Open in Gitpod

@github-actions github-actions Bot added the t-group-theory Group theory label May 11, 2026
@github-actions
Copy link
Copy Markdown

PR summary 260979c9dd

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.


No changes to strong technical debt.
No changes to weak technical debt.

Comment thread Mathlib/GroupTheory/SpecificGroups/Alternating/Simple.lean
Copy link
Copy Markdown
Contributor

@tb65536 tb65536 left a comment

Choose a reason for hiding this comment

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

Nice, thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

t-group-theory Group theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants