Commit 2026-01-27 22:28 2a65b60c

View on Github →

refactor: Generalize Matrix.toEuclideanLin to PiLp (#34241) We can then recover the euclidean case as an abbrev. Also adds some lemmas about matrix multiplication.

Estimated changes

added theorem Matrix.ofLp_toLpLin
added def Matrix.toLpLin
added theorem Matrix.toLpLin_apply
added theorem Matrix.toLpLin_mul
added theorem Matrix.toLpLin_one
added theorem Matrix.toLpLin_pow
added theorem Matrix.toLpLin_symm_id
added theorem Matrix.toLpLin_toLp