Flow-direction additions vanish in a fivefold alternating form

Proved

BianchiIX.alternating_fin5_add_flow

by trppppp · Nov 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

bianchi-ix-era-statisticsdynamical-systems

For a real vector space $E$ , an alternating $5$ -linear form $f:E^5\to\mathbb R$ , vectors $X,F,A,B,C$ , and real $a,b,c$ ,

f(X,F,A+aF,B+bF,C+cF)=f(X,F,A,B,C).

Preamble

import Mathlib.LinearAlgebra.Determinant
import Mathlib.Data.Real.Basic
import Mathlib.Data.Fin.VecNotation
import Mathlib.Tactic.FinCases

namespace BianchiIX
end BianchiIX

noncomputable section
open BianchiIX
variable {E ι : Type*} [AddCommGroup E] [Module ℝ E] [Fintype ι] [DecidableEq ι]

Formal statement

theorem BianchiIX.alternating_fin5_add_flow (f : E [⋀^Fin 5]→ₗ[ℝ] ℝ)
    (X F A B C : E) (a b c : ℝ) :
    f ![X, F, A + a • F, B + b • F, C + c • F] = f ![X, F, A, B, C] := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/VolumeForms.lean#L44-L67

View graph