@[reducible, inline]

abbrev BCn.Space (n : ℕ) : Type

Equations

• BCn.Space n = (Fin n → ℤ)

@[reducible, inline]

abbrev BCn.CoSpace (n : ℕ) : Type

Equations

• BCn.CoSpace n = Module.Dual ℤ (BCn.Space n)

noncomputable def BCn.dotProduct (n : ℕ) : Space n →ₗ[ℤ] Space n →ₗ[ℤ] ℤ

The standard dot product on ℤⁿ.

Equations

• BCn.dotProduct n = { toFun := fun (x : BCn.Space n) => { toFun := fun (y : BCn.Space n) => ∑ i : Fin n, x i * y i, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

theorem BCn.dotProduct_apply (n : ℕ) (x y : Space n) : ((dotProduct n) x) y = ∑ i : Fin n, x i * y i

@[simp]

theorem BCn.dotProduct_single_right {n : ℕ} (x : Space n) (i : Fin n) : ((dotProduct n) x) (Pi.single i 1) = x i

@[simp]

theorem BCn.dotProduct_single_left {n : ℕ} (x : Space n) (i : Fin n) : ((dotProduct n) (Pi.single i 1)) x = x i

theorem BCn.dotProduct_isSymm (n : ℕ) : (dotProduct n).IsSymm

theorem BCn.dotProduct_nondegenerate (n : ℕ) : (dotProduct n).Nondegenerate

@[reducible, inline]

abbrev BCn.ReflectiveIndex (n : ℕ) : Type

The reflective vectors for the standard dot product.

Equations

• BCn.ReflectiveIndex n = { x : BCn.Space n // (BCn.dotProduct n).IsReflective x }

noncomputable def BCn.rootPairing (n : ℕ) : RootPairing (ReflectiveIndex n) ℤ (Space n) (CoSpace n)

The BCₙ root pairing, built from all reflective vectors for the standard dot product.

Equations

• BCn.rootPairing n = RootPairing.ofBilinear (BCn.dotProduct n) ⋯ ⋯ BCn.rootPairing._proof_3