RawExteriorPower.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.rawProduct line 14

Source documentation

Tensor product of scalar multilinear forms before alternatization.

def rawProduct (a : MultilinearMap ℝ (fun _ : ι => E) ℂ)
    (b : MultilinearMap ℝ (fun _ : κ => E) ℂ) :
    MultilinearMap ℝ (fun _ : ι ⊕ κ => E) ℂ :=
…

lemma OAI.Mahler.rawProduct_apply line 20
theorem OAI.Mahler.rawProduct_alternatization line 26
Source documentation
The actual shuffle normalization is exactly full alternatization of a raw tensor product; no factorial is silently inserted.
```
theorem rawProduct_alternatization (a : MultilinearMap ℝ (fun _ : ι => E) ℂ)
    (b : MultilinearMap ℝ (fun _ : κ => E) ℂ) :
    (rawProduct a b).alternatization = wedge a.alternatization b.alternatization := by
…
```
Mentions: OAI.Mahler.rawProduct, OAI.Mahler.wedge

def OAI.Mahler.rawPower line 34

Source documentation

The raw ordered product of k bilinear factors.

def rawPower (B : MultilinearMap ℝ (fun _ : Fin 2 => E) ℂ) :
    (k : ℕ) → MultilinearMap ℝ (fun _ : WedgePowerSlots k => E) ℂ
  | 0 => MultilinearMap.constOfIsEmpty ℝ (fun _ : Fin 0 => E) (1 : ℂ)
  | k+1 => rawProduct B (rawPower B k)

Mentions: OAI.Mahler.WedgePowerSlots, OAI.Mahler.rawProduct

theorem OAI.Mahler.rawPower_alternatization line 39
def OAI.Mahler.rawCovector line 54
lemma OAI.Mahler.rawCovector_apply line 57
lemma OAI.Mahler.rawCovector_alternatization line 59
def OAI.Mahler.rawBoundary line 64
theorem OAI.Mahler.rawBoundary_alternatization line 68