Documentation
Atlas
.
AlgebraNotes
.
code
.
PGroups
Search
return to top
source
Imports
Init
Mathlib.GroupTheory.PGroup
Imported by
PGroups
.
p_group_center_nontrivial
source
theorem
PGroups
.
p_group_center_nontrivial
{
p
:
ℕ
}
[
Fact
(
Nat.Prime
p
)
]
{
G
:
Type
u_1}
[
Group
G
]
[
Finite
G
]
(
hG
:
IsPGroup
p
G
)
[
Nontrivial
G
]
:
Nontrivial
↥
(
Subgroup.center
G
)