Cancellation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Cancellation by a normal p-subgroup, the supporting lemma lem:pcore-cancellation of OpenAI, The Blockwise Alperin Weight Conjecture.

def OAI.PCoreCancellation.chainEquiv line 19
Source documentation
Strict enumeration identifies actual subgroup chains with the corresponding strict chains of nontrivial p-subgroups normalized by J.
```
noncomputable def chainEquiv (p : ℕ) (J : Subgroup X) :
    Chain p J ≃ FiniteChain.StrictChain (Allowed p J) where
…
```
Mentions: OAI.PCoreCancellation.Chain, OAI.FiniteChain.StrictChain, OAI.PCoreCancellation.Allowed
theorem OAI.PCoreCancellation.strict_list_pcore_cancellation line 33
Source documentation
A nontrivial p-core forces cancellation over strictly increasing lists of nontrivial p-subgroups normalized by J.
```
theorem strict_list_pcore_cancellation (p : ℕ) [Fact p.Prime] (J : Subgroup X)
    (hc : pCore p J ≠ ⊥) :
    (∑ l : FiniteChain.StrictChain (Allowed p J), (-1 : ℤ) ^ l.val.length) = 0 := by
…
```
Mentions: OAI.PCoreCancellation.pCore, OAI.FiniteChain.StrictChain, OAI.PCoreCancellation.Allowed
theorem OAI.PCoreCancellation.cancellation line 42
Source documentation
The signed sum over strict p-subgroup chains beginning at the trivial subgroup and stabilized by J vanishes when the p-core of J is nontrivial.
```
theorem cancellation (p : ℕ) [Fact p.Prime] (J : Subgroup X)
    (hc : pCore p J ≠ ⊥) :
    (∑ l : Chain p J, (-1 : ℤ) ^ l.val.length) = 0 := by
…
```
Mentions: OAI.PCoreCancellation.pCore, OAI.PCoreCancellation.Chain
theorem OAI.PCoreCancellation.weight_eq_zero line 54