FinsetCancellation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Alternating cancellation over finite chains of p-subgroups normalized by J.

def OAI.PCoreCancellation.Allowed line 18
Source documentation
A p-subgroup normalized by J.
```
def Allowed (p : ℕ) (J Q : Subgroup X) : Prop :=
…
```
def OAI.PCoreCancellation.chainWeight line 23
Source documentation
The signed sum over chains of nontrivial p-subgroups normalized by J, with the trivial subgroup understood as the first term of each chain.
```
noncomputable def chainWeight (p : ℕ) (J : Subgroup X) : ℤ := by
…
```
theorem OAI.PCoreCancellation.cancellation_of_normal_p_subgroup line 27
theorem OAI.PCoreCancellation.pcore_cancellation line 41
Source documentation
A nontrivial p-core makes the alternating chain sum vanish.
```
theorem pcore_cancellation (p : ℕ) [Fact p.Prime] (J : Subgroup X)
    (hc : pCore p J ≠ ⊥) : chainWeight p J = 0 := by
…
```
Mentions: OAI.PCoreCancellation.pCore, OAI.PCoreCancellation.chainWeight