Mission prelude: the Mathlib vocabulary the milestones use
Definitionhefferon_preludelinear-algebraprelude
A prelude module for the mission. It carries no mathematical content of its own; it exists so that the milestone statements can name the Mathlib notions Hefferon's book uses -- bases, inner product spaces and orthogonal complements, and the characteristic polynomial of a matrix.
Definition code
import Mathlib namespace HefferonLinAlg /-- A basis of `V` over `K` indexed by `iota`, in Hefferon's sense: an ordered linearly independent spanning family (Two.III.1). -/ abbrev IsBasisIndexedBy (iota K V : Type*) [Field K] [AddCommGroup V] [Module K V] := Module.Basis iota K V end HefferonLinAlg
Source
Jim Hefferon, *Linear Algebra*, Saint Michael's College, 2020 printing