CovectorVolume.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.covectorVolume line 13
Source documentation
The alternating product of a family of real-linear complex covectors.
```
noncomputable def covectorVolume (l : ι → T →ₗ[ℝ] ℂ) : T [⋀^ι]→ₗ[ℝ] ℂ :=
…
```
lemma OAI.Mahler.covectorVolume_apply line 16
theorem OAI.Mahler.wedge_covectorVolume line 25
Source documentation
Exterior multiplication of simple forms concatenates their covectors, with the exact shuffle normalization and slot order.
```
theorem wedge_covectorVolume (l : ι → T →ₗ[ℝ] ℂ) (r : κ → T →ₗ[ℝ] ℂ) :
    wedge (covectorVolume l) (covectorVolume r) = covectorVolume (Sum.elim l r) := by
…
```
Mentions: OAI.Mahler.wedge, OAI.Mahler.covectorVolume
lemma OAI.Mahler.wedge_sum_left line 36
lemma OAI.Mahler.wedge_sum_right line 41

theorem OAI.Mahler.covectorVolume_linearCombination line 47

Source documentation

A change of covectors multiplies the associated volume by its determinant.

theorem covectorVolume_linearCombination (C : Matrix ι ι ℂ) (l : ι → T →ₗ[ℝ] ℂ) :
    covectorVolume (fun j => ∑ k, C j k • l k) = C.det • covectorVolume l := by
…

Mentions: OAI.Mahler.covectorVolume

lemma OAI.Mahler.covectorVolume_reindex_apply line 65