Eig3x3.Basic — types and the 3×3 vector/matrix vocabulary

Core types (Vec3, Eigval3, Mat3, SymmMat3, Decomposition), the public Float arithmetic vocabulary, typeclass instances for arithmetic notation, and scoped unicode notation.

Usage

Importing this module activates every typeclass instance (Add, Mul, HSMul, Inv, …), so arithmetic on Vec3 and Mat3 works immediately through Lean's core syntax. The Unicode operator glyphs are opt-in:

open scoped Eig3x3

Notation and Operators

A Mathlib-consistent operator layer for vector/matrix algebra on Float, with no Mathlib dependency. Precedences follow Lean core and Mathlib:

Notation	Operation	Declaration	Convention source
a + b	addition	infixl:65	Lean core (HAdd.hAdd)
a - b	subtraction	infixl:65	Lean core (HSub.hSub)
-a	negation	prefix	Lean core (Neg.neg)
a * b	multiplication/action	infixl:70	Lean core (HMul.hMul)
a / s	scalar division	infixl:70	Lean core (HDiv.hDiv)
u ⊗ᵥ v	vector outer product	infixl:70	(new; subscript family of ⬝ᵥ)
u ⬝ᵥ v	vector dot product	infixl:72	Mathlib Matrix.dotProduct
A ⬝ₘ B	matrix Frobenius dot	infixl:72	(family extension of ⬝ᵥ)
s • v	scalar multiplication	infixr:73	Lean core (HSMul.hSMul)
u ⨯₃ v	cross product	infixl:74	Mathlib crossProduct
x ^ⁿ n	power (by fast Nat)	infixr:80	(new; family of ^)
A ⊙ B	Hadamard product	infixl:100	Mathlib Matrix.hadamard
|x|	absolute value	delimited	Mathlib |a| for abs
‖v‖	norm	delimited	Mathlib Norm.norm
‖v‖²	squared norm	delimited	(Mathlib writes ‖x‖ ^ 2)
Aᵀ	transpose	postfix:max	Mathlib Matrix.transpose
A⁻¹	inverse	postfix:max	Lean core (Inv.inv)

Binding strength: + - (65) < * / (70) < ⬝ᵥ ⬝ₘ (72) < • (73) < ⨯₃ (74) < ^ⁿ (80) < ⊙ (100); the postfixes ᵀ and ⁻¹ (1024) bind tightest.

Useful consequences:

• u ⬝ᵥ v ⨯₃ w parses as u ⬝ᵥ (v ⨯₃ w) — the scalar triple product needs no parentheses.
• s • u ⨯₃ v parses as s • (u ⨯₃ v).
• u ⬝ᵥ u + v ⬝ᵥ v parses as (u ⬝ᵥ u) + (v ⬝ᵥ v).
• M⁻¹ᵀ parses as (M⁻¹)ᵀ.

Important: ⬝ᵥ (72) binds tighter than * (70), so M * v ⬝ᵥ w parses as M * (v ⬝ᵥ w) — write (M * v) ⬝ᵥ w instead.

structure Eig3x3.Vec3 : Type

Vector over Float in real (ℝ³) space.

• x : Float

  X coordinate (first component).

• y : Float

  Y coordinate (second component).

• z : Float

  Z coordinate (third component).

def Eig3x3.instReprVec3.repr : Vec3 → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Eig3x3.instReprVec3 : Repr Vec3

Equations

• Eig3x3.instReprVec3 = { reprPrec := Eig3x3.instReprVec3.repr }

structure Eig3x3.Mat3 : Type

General 3×3 matrix over Float, stored by columns. The primary matrix this library produces is the eigenvector matrix Q, whose columns are eigenvectors, matching conventional mathematics and NumPy/SciPy/PyTorch.

• c₀ : Vec3

  Column 0 vector.

• c₁ : Vec3

  Column 1 vector.

• c₂ : Vec3

  Column 2 vector.

@[instance_reducible]

instance Eig3x3.instReprMat3 : Repr Mat3

Equations

• Eig3x3.instReprMat3 = { reprPrec := Eig3x3.instReprMat3.repr }

def Eig3x3.instReprMat3.repr : Mat3 → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

structure Eig3x3.SymmMat3 : Type

Symmetric 3×3 matrix stored as its six independent entries.

Meant to be used as an input parameter type, not for matrix math. Coerces one-way to Mat3 for matrix operations.

• a₀₀ : Float

  Diagonal entry A₀₀.

• a₁₁ : Float

  Diagonal entry A₁₁.

• a₂₂ : Float

  Diagonal entry A₂₂.

• a₀₁ : Float

  Off-diagonal entry A₀₁ = A₁₀.

• a₀₂ : Float

  Off-diagonal entry A₀₂ = A₂₀.

• a₁₂ : Float

  Off-diagonal entry A₁₂ = A₂₁.

@[instance_reducible]

instance Eig3x3.instReprSymmMat3 : Repr SymmMat3

Equations

• Eig3x3.instReprSymmMat3 = { reprPrec := Eig3x3.instReprSymmMat3.repr }

def Eig3x3.instReprSymmMat3.repr : SymmMat3 → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

structure Eig3x3.Eigval3 : Type

Ordered eigenvalues l₀ ≤ l₁ ≤ l₂.

Not meant to be used directly. A distinct return type so eigenvalue ordering guarantees required by Eberly's algorithm [Ebe14] are carried by the type. Coerces to Vec3 for vector operations. Coercion is one-way, and ordering guarantees do not hold after coercion.

• l₀ : Float

  Smallest eigenvalue.

• l₁ : Float

  Middle eigenvalue.

• l₂ : Float

  Largest eigenvalue.

def Eig3x3.instReprEigval3.repr : Eigval3 → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Eig3x3.instReprEigval3 : Repr Eigval3

Equations

• Eig3x3.instReprEigval3 = { reprPrec := Eig3x3.instReprEigval3.repr }

structure Eig3x3.Decomposition : Type

Full eigendecomposition: A = QΛQᵀ = Σᵢ λᵢ cᵢcᵢᵀ.

• eigvals : Eigval3

  Eigenvalues in increasing order: l₀ ≤ l₁ ≤ l₂.

• eigvecs : Mat3

  Eigenvector matrix Q; column cᵢ is a unit eigenvector for lᵢ. Right-handed: Q.det = 1.

@[instance_reducible]

instance Eig3x3.instReprDecomposition : Repr Decomposition

Equations

• Eig3x3.instReprDecomposition = { reprPrec := Eig3x3.instReprDecomposition.repr }

def Eig3x3.instReprDecomposition.repr : Decomposition → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

Vec3 operations

@[inline]

def Eig3x3.Vec3.add (u v : Vec3) : Vec3

Vector addition u + v.

Equations

• u.add v = { x := u.x + v.x, y := u.y + v.y, z := u.z + v.z }

@[inline]

def Eig3x3.Vec3.neg (v : Vec3) : Vec3

Vector negation -v.

Equations

• v.neg = { x := -v.x, y := -v.y, z := -v.z }

@[inline]

def Eig3x3.Vec3.sub (u v : Vec3) : Vec3

Vector subtraction u - v.

Equations

• u.sub v = { x := u.x - v.x, y := u.y - v.y, z := u.z - v.z }

@[inline]

def Eig3x3.Vec3.scale (v : Vec3) (s : Float) : Vec3

Scalar multiplication s • v.

Equations

• v.scale s = { x := s * v.x, y := s * v.y, z := s * v.z }

@[inline]

def Eig3x3.Vec3.div (v : Vec3) (s : Float) : Vec3

Scalar division v / s.

Equations

• v.div s = { x := 1.0 / s * v.x, y := 1.0 / s * v.y, z := 1.0 / s * v.z }

@[inline]

def Eig3x3.Vec3.dot (u v : Vec3) : Float

Vector dot product u ⬝ᵥ v.

Equations

• u.dot v = u.x * v.x + u.y * v.y + u.z * v.z

@[inline]

def Eig3x3.Vec3.cross (u v : Vec3) : Vec3

Vector cross product u ⨯₃ v in ℝ³.

Equations

• u.cross v = { x := u.y * v.z - u.z * v.y, y := u.z * v.x - u.x * v.z, z := u.x * v.y - u.y * v.x }

@[inline]

def Eig3x3.Vec3.normSq (u : Vec3) : Float

Squared Euclidean norm ‖u‖² = u.x² + u.y² + u.z².

Equations

• u.normSq = u.x * u.x + u.y * u.y + u.z * u.z

@[inline]

def Eig3x3.Vec3.norm (u : Vec3) : Float

Euclidean norm ‖u‖ = √(‖u‖²).

Equations

• u.norm = u.normSq.sqrt

@[inline]

def Eig3x3.Vec3.outer (u v : Vec3) : Mat3

Outer product of two vectors, producing the rank-1 matrix u vᵀ. Exposed as ⊗ᵥ. The columns are u scaled by the entries of v, matching Mat3's column-major layout.

Equations

• u.outer v = { c₀ := u.scale v.x, c₁ := u.scale v.y, c₂ := u.scale v.z }

@[inline]

def Eig3x3.Vec3.hadamard (u v : Vec3) : Vec3

Componentwise product, exposed as ⊙ via the Hadamard class. Vec3 deliberately has no Mul instance: the vector products of this library are ⬝ᵥ and ⨯₃, and ⊙ is the single entrywise spelling.

Equations

• u.hadamard v = { x := u.x * v.x, y := u.y * v.y, z := u.z * v.z }

@[inline]

def Eig3x3.Vec3.map (f : Float → Float) (v : Vec3) : Vec3

Componentwise map — workhorse for eigenvalue post-processing (clipping, shifting, reciprocals).

Equations

• Eig3x3.Vec3.map f v = { x := f v.x, y := f v.y, z := f v.z }

@[inline]

def Eig3x3.Vec3.map2 (f : Float → Float → Float) (u v : Vec3) : Vec3

Componentwise zip.

Equations

• Eig3x3.Vec3.map2 f u v = { x := f u.x v.x, y := f u.y v.y, z := f u.z v.z }

@[inline]

def Eig3x3.Vec3.abs (v : Vec3) : Vec3

Componentwise absolute value of a vector |v|.

Equations

• v.abs = Eig3x3.Vec3.map Float.abs v

@[inline]

def Eig3x3.Eigval3.toVec3 (e : Eigval3) : Vec3

Convert ordered eigenvalues Eigval3 to an unconstrained Vec3.

Equations

• e.toVec3 = { x := e.l₀, y := e.l₁, z := e.l₂ }

@[instance_reducible]

instance Eig3x3.instCoeEigval3Vec3 : Coe Eigval3 Vec3

One-way coercion: ordered eigenvalues are a vector, but an arbitrary vector is not ordered eigenvalues.

Equations

• Eig3x3.instCoeEigval3Vec3 = { coe := Eig3x3.Eigval3.toVec3 }

Mat3 operations

@[inline]

def Eig3x3.Mat3.transpose (M : Mat3) : Mat3

Rows become columns: nine field moves, no arithmetic.

Equations

• M.transpose = { c₀ := { x := M.c₀.x, y := M.c₁.x, z := M.c₂.x }, c₁ := { x := M.c₀.y, y := M.c₁.y, z := M.c₂.y }, c₂ := { x := M.c₀.z, y := M.c₁.z, z := M.c₂.z } }

@[inline]

def Eig3x3.Mat3.mulVec (M : Mat3) (v : Vec3) : Vec3

M·v: linear combination of the columns.

Equations

• M.mulVec v = ((M.c₀.scale v.x).add (M.c₁.scale v.y)).add (M.c₂.scale v.z)

@[inline]

def Eig3x3.Mat3.transposeMulVec (M : Mat3) (v : Vec3) : Vec3

Mᵀ·v without materializing the transpose: dot with each column.

Equations

• M.transposeMulVec v = { x := M.c₀.dot v, y := M.c₁.dot v, z := M.c₂.dot v }

@[inline]

def Eig3x3.Mat3.mul (M N : Mat3) : Mat3

M·N: column j of the product is M applied to column j of N.

Equations

• M.mul N = { c₀ := M.mulVec N.c₀, c₁ := M.mulVec N.c₁, c₂ := M.mulVec N.c₂ }

@[inline]

def Eig3x3.Mat3.scale (M : Mat3) (s : Float) : Mat3

Scalar multiplication of a matrix s • M.

Equations

• M.scale s = { c₀ := M.c₀.scale s, c₁ := M.c₁.scale s, c₂ := M.c₂.scale s }

@[inline]

def Eig3x3.Mat3.div (M : Mat3) (s : Float) : Mat3

Scalar division of a matrix M / s.

Equations

• M.div s = { c₀ := M.c₀.scale (1.0 / s), c₁ := M.c₁.scale (1.0 / s), c₂ := M.c₂.scale (1.0 / s) }

@[inline]

def Eig3x3.Mat3.add (M N : Mat3) : Mat3

Matrix addition M + N.

Equations

• M.add N = { c₀ := M.c₀.add N.c₀, c₁ := M.c₁.add N.c₁, c₂ := M.c₂.add N.c₂ }

@[inline]

def Eig3x3.Mat3.neg (M : Mat3) : Mat3

Matrix negation -M.

Equations

• M.neg = { c₀ := M.c₀.neg, c₁ := M.c₁.neg, c₂ := M.c₂.neg }

@[inline]

def Eig3x3.Mat3.sub (M N : Mat3) : Mat3

Matrix subtraction M - N.

Equations

• M.sub N = { c₀ := M.c₀.sub N.c₀, c₁ := M.c₁.sub N.c₁, c₂ := M.c₂.sub N.c₂ }

@[inline]

def Eig3x3.Mat3.hadamard (M N : Mat3) : Mat3

Componentwise (Hadamard) product, exposed as ⊙.

Equations

• M.hadamard N = { c₀ := M.c₀.hadamard N.c₀, c₁ := M.c₁.hadamard N.c₁, c₂ := M.c₂.hadamard N.c₂ }

@[inline]

def Eig3x3.Mat3.abs (M : Mat3) : Mat3

Componentwise absolute value.

Equations

• M.abs = { c₀ := M.c₀.abs, c₁ := M.c₁.abs, c₂ := M.c₂.abs }

@[inline]

def Eig3x3.Mat3.dot (M N : Mat3) : Float

Matrix Frobenius inner product ∑ᵢⱼ Mᵢⱼ Nᵢⱼ = tr(MᵀN).

Equations

• M.dot N = M.c₀.dot N.c₀ + M.c₁.dot N.c₁ + M.c₂.dot N.c₂

@[inline]

def Eig3x3.Mat3.normSq (M : Mat3) : Float

Squared Frobenius norm: sum of squares of all entries.

Equations

• M.normSq = M.c₀.normSq + M.c₁.normSq + M.c₂.normSq

@[inline]

def Eig3x3.Mat3.norm (M : Mat3) : Float

Frobenius norm: square root of sum of squares of all entries. (Not the operator norm; chosen because it is exactly computable with nine multiplications.)

Equations

• M.norm = M.normSq.sqrt

@[inline]

def Eig3x3.Mat3.det (M : Mat3) : Float

det M: the triple product (c₀ × c₁) ⬝ c₂ of the columns.

Equations

• M.det = (M.c₀.cross M.c₁).dot M.c₂

@[inline]

def Eig3x3.Mat3.trace (M : Mat3) : Float

tr M: sum of the diagonal entries.

Equations

• M.trace = M.c₀.x + M.c₁.y + M.c₂.z

def Eig3x3.Mat3.id : Mat3

The identity matrix.

Equations

• Eig3x3.Mat3.id = { c₀ := { x := 1.0, y := 0.0, z := 0.0 }, c₁ := { x := 0.0, y := 1.0, z := 0.0 }, c₂ := { x := 0.0, y := 0.0, z := 1.0 } }

@[inline]

def Eig3x3.Mat3.ofRows (r₀ r₁ r₂ : Vec3) : Mat3

Row-minded constructor: build from three rows.

Equations

• Eig3x3.Mat3.ofRows r₀ r₁ r₂ = { c₀ := r₀, c₁ := r₁, c₂ := r₂ }.transpose

def Eig3x3.Mat3.inv (M : Mat3) : Mat3

Invert a 3×3 matrix via cofactor cross products: M⁻¹ = (1/det M) adj(M), with adj(M) computed from cross products of the rows. Totalized like the rest of the Float vocabulary: a singular M yields inf/NaN entries rather than an error.

Equations

• One or more equations did not get rendered due to their size.

def Eig3x3.SymmMat3.toMat3 (A : SymmMat3) : Mat3

Convert a symmetric matrix representation SymmMat3 to a full Mat3.

Equations

• A.toMat3 = { c₀ := { x := A.a₀₀, y := A.a₀₁, z := A.a₀₂ }, c₁ := { x := A.a₀₁, y := A.a₁₁, z := A.a₁₂ }, c₂ := { x := A.a₀₂, y := A.a₁₂, z := A.a₂₂ } }

@[instance_reducible]

instance Eig3x3.instCoeSymmMat3Mat3 : Coe SymmMat3 Mat3

One-way coercion: a symmetric matrix is a matrix, but an arbitrary matrix is not symmetric.

Equations

• Eig3x3.instCoeSymmMat3Mat3 = { coe := Eig3x3.SymmMat3.toMat3 }

Fast natural-number powers (^ⁿ)

class Eig3x3.PowNat (α : Type) : Type

Fast natural-number power, exposed as x ^ⁿ n.

• powNat : α → Nat → α

  Exponentiate x to natural power n.

def Eig3x3.powNatSmall (x : Float) : Nat → Float

Power by repeated multiplication — adequate for the small exponents (e.g. 2 or 3) that appear in characteristic-polynomial computations, and computationally cheaper than Lean's C-accelerated pow call.

Equations

• Eig3x3.powNatSmall x 0 = 1.0
• Eig3x3.powNatSmall x n.succ = x * Eig3x3.powNatSmall x n

@[instance_reducible]

instance Eig3x3.instPowNatFloat : PowNat Float

Conditioning for Float: repeated multiplication below 8, core's C-accelerated Float.pow above 8.

Equations

• Eig3x3.instPowNatFloat = { powNat := fun (x : Float) (n : Nat) => if n ≤ 8 then Eig3x3.powNatSmall x n else x.pow n.toFloat }

partial def Eig3x3.Mat3.powSq (M : Mat3) (n : Nat) : Mat3

Conditioning for Mat3: exponentiation by squaring, ⌈log₂ n⌉ matrix products instead of n, with M ^ⁿ 0 = Mat3.id.

@[instance_reducible]

instance Eig3x3.instPowNatMat3 : PowNat Mat3

Equations

• Eig3x3.instPowNatMat3 = { powNat := Eig3x3.Mat3.powSq }

@[instance_reducible]

instance Eig3x3.instPowMat3Nat : Pow Mat3 Nat

Flexible compatibility with core's ^.

Equations

• Eig3x3.instPowMat3Nat = { pow := Eig3x3.Mat3.powSq }

Custom typeclasses behind the delimited/Hadamard notation

class Eig3x3.Abs (α : Type) : Type

Absolute value behind a typeclass, so the same bars work on Float (magnitude), Vec3 (componentwise), and Mat3 (componentwise).

• abs : α → α

  Absolute value / componentwise magnitude.

@[instance_reducible]

instance Eig3x3.instAbsFloat : Abs Float

Equations

• Eig3x3.instAbsFloat = { abs := Float.abs }

@[instance_reducible]

instance Eig3x3.instAbsVec3 : Abs Vec3

Equations

• Eig3x3.instAbsVec3 = { abs := Eig3x3.Vec3.abs }

@[instance_reducible]

instance Eig3x3.instAbsMat3 : Abs Mat3

Equations

• Eig3x3.instAbsMat3 = { abs := Eig3x3.Mat3.abs }

class Eig3x3.Norm (α : Type) : Type

Euclidean norm for vectors, Frobenius norm for matrices.

• norm : α → Float

  Euclidean (vector) or Frobenius (matrix) norm.

@[instance_reducible]

instance Eig3x3.instNormVec3 : Norm Vec3

Equations

• Eig3x3.instNormVec3 = { norm := Eig3x3.Vec3.norm }

@[instance_reducible]

instance Eig3x3.instNormMat3 : Norm Mat3

Equations

• Eig3x3.instNormMat3 = { norm := Eig3x3.Mat3.norm }

class Eig3x3.NormSq (α : Type) : Type

Squared norm: Euclidean for vectors, Frobenius for matrices.

• normSq : α → Float

  Squared norm.

@[instance_reducible]

instance Eig3x3.instNormSqVec3 : NormSq Vec3

Equations

• Eig3x3.instNormSqVec3 = { normSq := Eig3x3.Vec3.normSq }

@[instance_reducible]

instance Eig3x3.instNormSqMat3 : NormSq Mat3

Equations

• Eig3x3.instNormSqMat3 = { normSq := Eig3x3.Mat3.normSq }

class Eig3x3.Hadamard (α : Type) : Type

Hadamard (componentwise) product.

• hadamard : α → α → α

  Componentwise (Hadamard) product.

@[instance_reducible]

instance Eig3x3.instHadamardVec3 : Hadamard Vec3

Equations

• Eig3x3.instHadamardVec3 = { hadamard := Eig3x3.Vec3.hadamard }

@[instance_reducible]

instance Eig3x3.instHadamardMat3 : Hadamard Mat3

Equations

• Eig3x3.instHadamardMat3 = { hadamard := Eig3x3.Mat3.hadamard }

Arithmetic instances (global: these are this package's own types)

@[instance_reducible]

instance Eig3x3.instAddVec3 : Add Vec3

Equations

• Eig3x3.instAddVec3 = { add := Eig3x3.Vec3.add }

@[instance_reducible]

instance Eig3x3.instNegVec3 : Neg Vec3

Equations

• Eig3x3.instNegVec3 = { neg := Eig3x3.Vec3.neg }

@[instance_reducible]

instance Eig3x3.instSubVec3 : Sub Vec3

Equations

• Eig3x3.instSubVec3 = { sub := Eig3x3.Vec3.sub }

@[instance_reducible]

instance Eig3x3.instHSMulFloatVec3 : HSMul Float Vec3 Vec3

Equations

• Eig3x3.instHSMulFloatVec3 = { hSMul := fun (s : Float) (v : Eig3x3.Vec3) => v.scale s }

@[instance_reducible]

instance Eig3x3.instHDivVec3Float : HDiv Vec3 Float Vec3

Equations

• Eig3x3.instHDivVec3Float = { hDiv := Eig3x3.Vec3.div }

@[instance_reducible]

instance Eig3x3.instAddMat3 : Add Mat3

Equations

• Eig3x3.instAddMat3 = { add := Eig3x3.Mat3.add }

@[instance_reducible]

instance Eig3x3.instNegMat3 : Neg Mat3

Equations

• Eig3x3.instNegMat3 = { neg := Eig3x3.Mat3.neg }

@[instance_reducible]

instance Eig3x3.instSubMat3 : Sub Mat3

Equations

• Eig3x3.instSubMat3 = { sub := Eig3x3.Mat3.sub }

@[instance_reducible]

instance Eig3x3.instMulMat3 : Mul Mat3

Equations

• Eig3x3.instMulMat3 = { mul := Eig3x3.Mat3.mul }

@[instance_reducible]

instance Eig3x3.instHMulMat3Vec3 : HMul Mat3 Vec3 Vec3

Equations

• Eig3x3.instHMulMat3Vec3 = { hMul := Eig3x3.Mat3.mulVec }

@[instance_reducible]

instance Eig3x3.instHMulVec3Mat3 : HMul Vec3 Mat3 Vec3

Row-vector times matrix product vᵀ M without materializing the transpose.

Equations

• Eig3x3.instHMulVec3Mat3 = { hMul := fun (v : Eig3x3.Vec3) (M : Eig3x3.Mat3) => M.transposeMulVec v }

@[instance_reducible]

instance Eig3x3.instHSMulFloatMat3 : HSMul Float Mat3 Mat3

Equations

• Eig3x3.instHSMulFloatMat3 = { hSMul := fun (s : Float) (M : Eig3x3.Mat3) => M.scale s }

@[instance_reducible]

instance Eig3x3.instHDivMat3Float : HDiv Mat3 Float Mat3

Equations

• Eig3x3.instHDivMat3Float = { hDiv := Eig3x3.Mat3.div }

@[instance_reducible]

instance Eig3x3.instInvMat3 : Inv Mat3

Matrix inverse through Lean core's Inv class, so M⁻¹ just works.

Equations

• Eig3x3.instInvMat3 = { inv := Eig3x3.Mat3.inv }

Scoped operators (open scoped Eig3x3 to activate)

def Eig3x3.«term_⊗ᵥ_» : Lean.TrailingParserDescr

Outer product producing the rank-1 matrix u vᵀ. Type \otimes then \_v.

Equations

• Eig3x3.«term_⊗ᵥ_» = Lean.ParserDescr.trailingNode `Eig3x3.«term_⊗ᵥ_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ᵥ ") (Lean.ParserDescr.cat `term 71))

def Eig3x3.«term_⬝ᵥ_» : Lean.TrailingParserDescr

Vector dot product. Type \cdot then \_v (or \dot\_v).

Equations

• Eig3x3.«term_⬝ᵥ_» = Lean.ParserDescr.trailingNode `Eig3x3.«term_⬝ᵥ_» 72 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⬝ᵥ ") (Lean.ParserDescr.cat `term 73))

def Eig3x3.«term_⬝ₘ_» : Lean.TrailingParserDescr

Matrix Frobenius inner product. Type \cdot\_m.

Equations

• Eig3x3.«term_⬝ₘ_» = Lean.ParserDescr.trailingNode `Eig3x3.«term_⬝ₘ_» 72 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⬝ₘ ") (Lean.ParserDescr.cat `term 73))

def Eig3x3.«term_⨯₃_» : Lean.TrailingParserDescr

Cross product (⨯₃, U+2A2F). Type \crossproduct\_3.

Equations

• Eig3x3.«term_⨯₃_» = Lean.ParserDescr.trailingNode `Eig3x3.«term_⨯₃_» 74 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⨯₃ ") (Lean.ParserDescr.cat `term 75))

def Eig3x3.«term|___|» : Lean.ParserDescr

Absolute value bars, whitespace-sensitive: the bars must hug the argument (|v|, never | v |), so the leading bar will not be mistaken for | in match, which is always followed by a space.

Equations

• One or more equations did not get rendered due to their size.

def Eig3x3.«term_^ⁿ_» : Lean.TrailingParserDescr

Fast natural-number exponent operator. Right-associative. Type ^\^n.

Equations

• Eig3x3.«term_^ⁿ_» = Lean.ParserDescr.trailingNode `Eig3x3.«term_^ⁿ_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^ⁿ ") (Lean.ParserDescr.cat `term 80))

def Eig3x3.«term‖_‖» : Lean.ParserDescr

Norm: Euclidean on Vec3, Frobenius on Mat3. Type \Vert.

Equations

• One or more equations did not get rendered due to their size.

def Eig3x3.«term‖_‖²» : Lean.ParserDescr

Squared norm. Write it tight: ‖v‖², no space before the ².

Equations

• One or more equations did not get rendered due to their size.

def Eig3x3.«term_⊙_» : Lean.TrailingParserDescr

Hadamard (componentwise) product. Type \odot.

Equations

• Eig3x3.«term_⊙_» = Lean.ParserDescr.trailingNode `Eig3x3.«term_⊙_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊙ ") (Lean.ParserDescr.cat `term 101))

def Eig3x3.«term_ᵀ» : Lean.TrailingParserDescr

Transpose. Type \^T.

Equations

• Eig3x3.«term_ᵀ» = Lean.ParserDescr.trailingNode `Eig3x3.«term_ᵀ» 1024 1024 (Lean.ParserDescr.symbol "ᵀ")

Internal pipeline helpers (package-private)