Core.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The p-core of a subgroup, represented inside the ambient group.

def OAI.PCoreCancellation.NormalPIn line 14
Source documentation
A p-subgroup of J normalized by every element of J.
```
def NormalPIn (p : ℕ) (J P : Subgroup X) : Prop :=
…
```
def OAI.PCoreCancellation.pCore line 18
Source documentation
The ambient image of the p-core of J.
```
noncomputable def pCore (p : ℕ) (J : Subgroup X) : Subgroup X :=
…
```
theorem OAI.PCoreCancellation.exists_normal_p_subgroup line 21
lemma OAI.PCoreCancellation.normalPIn_bot line 35
lemma OAI.PCoreCancellation.normalPIn_sup line 44
theorem OAI.PCoreCancellation.pCore_normalPIn line 59
Source documentation
The p-core is a normal p-subgroup of J.
```
theorem pCore_normalPIn (p : ℕ) [Fact p.Prime] (J : Subgroup X) :
    NormalPIn p J (pCore p J) := by
…
```
Mentions: OAI.PCoreCancellation.NormalPIn, OAI.PCoreCancellation.pCore
theorem OAI.PCoreCancellation.pCore_greatest line 85
Source documentation
The p-core is the greatest normal p-subgroup of J.
```
theorem pCore_greatest (p : ℕ) [Fact p.Prime] (J : Subgroup X) :
    NormalPIn p J (pCore p J) ∧
      ∀ Q : Subgroup X, NormalPIn p J Q → Q ≤ pCore p J :=
…
```
Mentions: OAI.PCoreCancellation.NormalPIn, OAI.PCoreCancellation.pCore
theorem OAI.PCoreCancellation.pCore_eq_of_greatest line 90