Skip to content

feat(LinearAlgebra/Projectivization/Action): prove that the action is 2-transitive and primitive#33715

Open
AntoineChambert-Loir wants to merge 269 commits intoleanprover-community:masterfrom
AntoineChambert-Loir:ACL/SL-projectivization
Open

feat(LinearAlgebra/Projectivization/Action): prove that the action is 2-transitive and primitive#33715
AntoineChambert-Loir wants to merge 269 commits intoleanprover-community:masterfrom
AntoineChambert-Loir:ACL/SL-projectivization

Conversation

@AntoineChambert-Loir
Copy link
Copy Markdown
Collaborator

@AntoineChambert-Loir AntoineChambert-Loir commented Jan 7, 2026 •
edited
Loading

AntoineChambert-Loir and others added 30 commits October 22, 2025 10:27
@AntoineChambert-Loir
Merge branch 'master' into ACL-QuadraticAlgebra
5370ac1
@AntoineChambert-Loir
adjust
fc67393
@AntoineChambert-Loir
one argument is not implicit
03aa4e0
@AntoineChambert-Loir
initial commmit
d14f731
@AntoineChambert-Loir
add head docstring
9261aeb
@AntoineChambert-Loir
basis stuff for special linear group
ce782ff
@pre-commit-ci-lite
[pre-commit.ci lite] apply automatic fixes
0c8812f
@AntoineChambert-Loir
add file in Mathlib.lean
4135313
@AntoineChambert-Loir
Merge branch 'ACL/SL' of github.com:AntoineChambert-Loir/mathlib4 int…
3d26290 
…o ACL/SL
@AntoineChambert-Loir
adjust
90f2d0f
@AntoineChambert-Loir
delete QuadraticAlgebra/Basic
a9b4138
@AntoineChambert-Loir
Update Mathlib/Algebra/Group/Basic.lean
c4087e2
@AntoineChambert-Loir
Update Mathlib/Algebra/QuadraticAlgebra.lean
3bfad53
@AntoineChambert-Loir
Update Mathlib/Algebra/QuadraticAlgebra.lean
3ac6193
@AntoineChambert-Loir
Update Mathlib/Algebra/QuadraticAlgebra.lean
38bed50
@AntoineChambert-Loir
Update Mathlib/Algebra/QuadraticAlgebra.lean
c6e365c
@AntoineChambert-Loir
Update Mathlib/Algebra/QuadraticAlgebra.lean
3160e96
@AntoineChambert-Loir
adjust once more
3fd7b2d
@AntoineChambert-Loir
Merge branch 'master' into ACL/SL
1ba35ac
@AntoineChambert-Loir
add docstring
bc74e84
@AntoineChambert-Loir
Merge branch 'ACL/SL' of github.com:AntoineChambert-Loir/mathlib4 int…
4aa6626 
…o ACL/SL
@AntoineChambert-Loir
Update Mathlib/LinearAlgebra/Determinant.lean
28a7931
@AntoineChambert-Loir
Update Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
fc5c7be
@AntoineChambert-Loir
Update Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
2f55e28
@AntoineChambert-Loir
Update Mathlib/Topology/Algebra/Module/FiniteDimension.lean
2be7690
@AntoineChambert-Loir
Update Mathlib/LinearAlgebra/Determinant.lean
9446cac
@AntoineChambert-Loir
Update Mathlib/Topology/Algebra/Module/FiniteDimension.lean
fd835b0
@AntoineChambert-Loir
Update Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
518665a
@AntoineChambert-Loir
Update Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
979e5d4
@AntoineChambert-Loir
adjust, add doc
f08260b
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Jan 24, 2026

This pull request has conflicts, please merge master and resolve them.

@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 24, 2026
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 24, 2026
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Jan 26, 2026

This pull request has conflicts, please merge master and resolve them.

@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 26, 2026
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 6, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Feb 13, 2026

This pull request has conflicts, please merge master and resolve them.

@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 13, 2026
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 16, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 17, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Feb 17, 2026

This pull request has conflicts, please merge master and resolve them.

@mathlib-dependent-issues mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 26, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Mar 26, 2026

This PR/issue depends on:

@github-actions github-actions bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) file-removed A Lean module was (re)moved without a `deprecated_module` annotation labels Mar 30, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

@joelriou joelriou

Labels

large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@AntoineChambert-Loir @mathlib4-merge-conflict-bot @joelriou @mathlib4-dependent-issues-bot