WedgeEven.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Mahler.wedge_reindex line 13
lemma OAI.Mahler.two_block_swap_sign line 33
Source documentation
The swap of two two-slot blocks has positive sign.
```
lemma two_block_swap_sign : Equiv.Perm.sign (Equiv.sumComm (Fin 2) (Fin 2)) = 1 := by
…
```
lemma OAI.Mahler.wedge_two_comm line 36

lemma OAI.Mahler.wedge_two_left_comm line 43

Source documentation

Two degree-two factors commute in their original nested slot order.

lemma wedge_two_left_comm (basis : Module.Basis J ℝ T)
    (a b : T [⋀^Fin 2]→ₗ[ℝ] ℂ) (c : T [⋀^ν]→ₗ[ℝ] ℂ) :
    wedge a (wedge b c) = wedge b (wedge a c) := by
…

Mentions: OAI.Mahler.wedge

lemma OAI.Mahler.wedge_add_left line 48
lemma OAI.Mahler.wedge_add_right line 53
theorem OAI.Mahler.wedgePowerVariation_succ line 60
Source documentation
The k+1 genuine variation placements are equal, with no suppressed signs or reassociations. This is the multiplicity in homogeneous transgression.
```
theorem wedgePowerVariation_succ (basis : Module.Basis J ℝ T)
    (a da : T [⋀^Fin 2]→ₗ[ℝ] ℂ) (k : ℕ) :
    wedgePowerVariation a da (k+1) =
      ((k+1 : ℕ) : ℂ) • wedge da (wedgePower a k) := by
…
```
Mentions: OAI.Mahler.wedgePowerVariation, OAI.Mahler.wedge, OAI.Mahler.wedgePower