本人是2025级学院路校区王磊老师班的学生，在此将本人本学习复习资料开源，方便后来者复习。包括本人的复习笔记，往年真题，教科书和考试大纲。
This Repository Contains all the Lecture Notes, Assignments, Coding Problems and Everything of M.Tech AI at IIT Hyderabad 2023-2025
A complete Lean 4 formalization of the nonsingularity of Colombo's 1928 difference-power determinant.
矩阵的LU分解的数值实验
An algorithm for computing the k-numerical range
Lean 4 formal verification of arithmetic matrix properties related to the Riemann Hypothesis. Includes machine-checked rank, coercivity, and impossibility theorems for the SR/Rees comparison matrix program, plus a complete research ledger of proved results, killed approaches, and the identified analytic frontier.
Investigation into Mathematics.
lean 4 theorems
Technical review of invariant two-parameter families of circulant sparse matrices and their applications in correlation signal theory.
Lean 4 / Mathlib Schur complement nonsing_inv API and block inverse lemmas.
To associate your repository with the matrix-theory topic, visit your repo's landing page and select "manage topics."