def ExteriorAlgebra.wedge {R : Type u_1} [CommRing R] {n : ℕ} (v w : Fin n → R) : Matrix (Fin n) (Fin n) R

@[simp]

theorem ExteriorAlgebra.wedge_apply {R : Type u_1} [CommRing R] {n : ℕ} (v w : Fin n → R) (i j : Fin n) : wedge v w i j = v i * w j - w i * v j

theorem ExteriorAlgebra.wedge_transpose {R : Type u_1} [CommRing R] {n : ℕ} (v w : Fin n → R) : (wedge v w).transpose = -wedge v w

def ExteriorAlgebra.antisymmMatrices (n : ℕ) (R : Type u_2) [CommRing R] : Submodule R (Matrix (Fin n) (Fin n) R)

theorem ExteriorAlgebra.wedge_mem_antisymm {R : Type u_1} [CommRing R] {n : ℕ} (v w : Fin n → R) : wedge v w ∈ antisymmMatrices n R

@[reducible, inline]

abbrev ExteriorAlgebra.StrictUpperTriIdx (n : ℕ) : Type

theorem ExteriorAlgebra.wedge_stdBasis_upper {R : Type u_1} [CommRing R] {n : ℕ} [DecidableEq (Fin n)] (p q : StrictUpperTriIdx n) : wedge (Pi.single (↑p).1 1) (Pi.single (↑p).2 1) (↑q).1 (↑q).2 = if p = q then 1 else 0

theorem ExteriorAlgebra.wedge_isBasis {R : Type u_1} [CommRing R] {n : ℕ} [DecidableEq (Fin n)] [CharZero R] [NoZeroDivisors R] (b : Module.Basis (Fin n) R (Fin n → R)) : (LinearIndependent R fun (p : StrictUpperTriIdx n) => ⟨wedge (b (↑p).1) (b (↑p).2), ⋯⟩) ∧ Submodule.span R (Set.range fun (p : StrictUpperTriIdx n) => ⟨wedge (b (↑p).1) (b (↑p).2), ⋯⟩) = ⊤

@[reducible, inline]

abbrev ExteriorSquare.Idx (n : ℕ) : Type

def ExteriorSquare.matrix {R : Type u_1} [CommRing R] {n : ℕ} (L : Matrix (Fin n) (Fin n) R) : Matrix (Idx n) (Idx n) R

theorem ExteriorSquare.sum_sum_eq_two_sum_lt {R : Type u_1} [CommRing R] {n : ℕ} (f : Fin n → Fin n → R) (hdiag : ∀ (i : Fin n), f i i = 0) (hsymm : ∀ (i j : Fin n), f i j = f j i) : ∑ i : Fin n, ∑ j : Fin n, f i j = 2 * ∑ p : Idx n, f (↑p).1 (↑p).2

theorem ExteriorSquare.trace_exteriorSquare {R : Type u_1} [CommRing R] {n : ℕ} (L : Matrix (Fin n) (Fin n) R) : 2 * (matrix L).trace = L.trace ^ 2 - (L * L).trace

theorem ExteriorSquare.det_exteriorSquare {R : Type u_2} [CommRing R] {n : ℕ} [NeZero n] (L : Matrix (Fin n) (Fin n) R) : (matrix L).det = L.det ^ (n - 1)

theorem ExteriorSquare.exteriorSquare_trace_and_det {R : Type u_1} [CommRing R] {n : ℕ} [NeZero n] (L : Matrix (Fin n) (Fin n) R) : 2 * (matrix L).trace = L.trace ^ 2 - (L * L).trace ∧ (matrix L).det = L.det ^ (n - 1)

theorem ExteriorAlgebra.eq_or_eq_neg_of_exteriorPower_eq {n : ℕ} (L L' : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ) (hrank : 3 ≤ Module.finrank ℝ ↥L.range) (hΛ : ∀ (v w : Fin n → ℝ), wedge (L v) (L w) = wedge (L' v) (L' w)) : L = L' ∨ L = -L'