OAI/NumberTheory/DukePrimeDegree/Geometry/FrameChangeOfBasis.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Deriving the frame cocycle from subspace transport

Two full-rank finite frames with the same column space differ by an invertible matrix. This supplies the change of basis in the diagonal recurrence argument from transport of the actual velocity subspaces.

  1. theorem OAI.DukePrimeDegree.exists_invertible_frame_change line 20
  2. theorem OAI.DukePrimeDegree.linearIndependent_frame_of_minor line 44