Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - chore (Subgroup.Order): move ordered facts out of Basic and into Order #14121

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - chore (Subgroup.Order): move ordered facts out of Basic and into Order #14121

Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8dd2233
change
mattrobball Jun 25, 2024
9d3f819
update
mattrobball Jun 25, 2024
ff7d2a7
fix
mattrobball Jun 25, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Loading
Loading status checks…
fix
  • Loading branch information
@mattrobball
mattrobball committed Jun 25, 2024

Verified

This commit was signed with the committer’s verified signature.
mattrobball Matthew Robert Ballard
SSH Key Fingerprint: vQfTNiT1kLs4Qj1Svz0dYJYEDIhoY05quc0qFlmF7VU
Verified
Learn about vigilant mode
commit ff7d2a7681eec12a2771d96b490db0f5351b7dbe
1 change: 1 addition & 0 deletions Mathlib/Algebra/Group/Subgroup/Basic.lean
View file
Original file line number Diff line number Diff line change
@@ -83,6 +83,7 @@ membership of a subgroup's underlying set.
subgroup, subgroups
-/

assert_not_exists OrderedAddCommMonoid

open Function
open Int
1 change: 1 addition & 0 deletions Mathlib/GroupTheory/Nilpotent.lean
View file
Original file line number Diff line number Diff line change
@@ -9,6 +9,7 @@ import Mathlib.GroupTheory.PGroup
import Mathlib.GroupTheory.Sylow
import Mathlib.Data.Nat.Factorization.Basic
import Mathlib.Tactic.TFAE
import Mathlib.Algebra.Group.Subgroup.Order

#align_import group_theory.nilpotent from "leanprover-community/mathlib"@"2bbc7e3884ba234309d2a43b19144105a753292e"

3 changes: 2 additions & 1 deletion Mathlib/GroupTheory/Subgroup/Simple.lean
View file
Original file line number Diff line number Diff line change
@@ -3,7 +3,8 @@ Copyright (c) 2021 Aaron Anderson. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Aaron Anderson
-/
import Mathlib.Algebra.Group.Subgroup.Order
import Mathlib.Order.Atoms
import Mathlib.Algebra.Group.Subgroup.Basic

#align_import group_theory.subgroup.simple from "leanprover-community/mathlib"@"f93c11933efbc3c2f0299e47b8ff83e9b539cbf6"

Loading