ExteriorAlternatization.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.orderedInsertPermutation line 15
Source documentation
Insert the distinguished derivative slot at p, preserving the order of all remaining slots before applying their permutation.
```
def orderedInsertPermutation {n : ℕ} (p : Fin (n+1)) (σ : Equiv.Perm (Fin n)) :
    Equiv.Perm (Fin (n+1)) :=
…
```
lemma OAI.Mahler.orderedInsertPermutation_zero line 19
lemma OAI.Mahler.orderedInsertPermutation_succ line 23
lemma OAI.Mahler.orderedInsertPermutation_sign line 29
def OAI.Mahler.orderedPermutationEquiv line 37
Source documentation
An order-preserving decomposition of every permutation into its first image and a permutation of the remaining slots.
```
def orderedPermutationEquiv (n : ℕ) :
    (Fin (n+1) × Equiv.Perm (Fin n)) ≃ Equiv.Perm (Fin (n+1)) where
…
```
lemma OAI.Mahler.orderedPermutationEquiv_apply line 65
def OAI.Mahler.rawUncurry line 71
lemma OAI.Mahler.rawUncurry_apply line 78
theorem OAI.Mahler.alternatization_rawUncurry line 83
Source documentation
Full alternatization of a distinguished derivative slot contains each term of the usual exterior derivative exactly n! times.
```
theorem alternatization_rawUncurry {n : ℕ} (D : E →ₗ[ℝ] E [⋀^Fin n]→ₗ[ℝ] ℂ) :
    (rawUncurry D).alternatization = n.factorial • AlternatingMap.alternatizeUncurryFin D := by
…
```
Mentions: OAI.Mahler.rawUncurry

theorem OAI.Mahler.alternatization_uncurryLeft_apply line 106

Source documentation

General expansion: alternating all slots of an uncurried multilinear map is the signed sum of the alternatizations in its trailing slots.

theorem alternatization_uncurryLeft_apply {n : ℕ}
    (D : E →ₗ[ℝ] MultilinearMap ℝ (fun _ : Fin n => E) ℂ) (v : Fin (n+1) → E) :
    D.uncurryLeft.alternatization v =
      ∑ p : Fin (n+1), (-1 : ℤ)^p.val • (D (v p)).alternatization (p.removeNth v) := by
…