Basic.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PCoreCancellation.stabilizer line 13
Source documentation
The stabilizer of the chain beginning with the trivial subgroup and followed by the nodes in l.
```
def stabilizer (l : List (Subgroup X)) : Subgroup X :=
…
```
def OAI.PCoreCancellation.Chain line 19
Source documentation
A strict chain of p-subgroups with initial trivial subgroup, stabilized by J. The list records the nontrivial nodes, so its length is the chain length.
```
def Chain (p : ℕ) (J : Subgroup X) :=
…
```
lemma OAI.PCoreCancellation.stabilizer_condition line 23

theorem OAI.PCoreCancellation.normalizer_intersection_iff line 29

Source documentation

The trivial subgroup contributes the whole ambient group to the intersection of normalizers.

theorem normalizer_intersection_iff (J : Subgroup X) (s : Finset (Subgroup X)) :
    J ≤ Subgroup.normalizer ((⊥ : Subgroup X) : Set X) ⊓
      (⨅ Q ∈ s, Subgroup.normalizer (Q : Set X)) ↔
      ∀ Q ∈ s, J ≤ Subgroup.normalizer (Q : Set X) := by
…

instance OAI.PCoreCancellation.chainFintype line 37
def OAI.PCoreCancellation.weight line 54
Source documentation
The alternating sum over actual strict chains stabilized by J.
```
noncomputable def weight (p : ℕ) (J : Subgroup X) : ℤ :=
…
```