mathlib4_source_code_LinearAlgebra
具有向量空间结构意味着具有加法交换群
代码结构
- 基础概念
Basis（基础）
Dimension（维数）
FiniteDimensional（有限维）
FiniteDimensional.lean（有限维.lean）
FiniteSpan.lean（有限生成.lean）
Span（张成）
StdBasis.lean（标准基.lean）
- 矩阵与行列式
Matrix（矩阵）
Determinant.lean（行列式.lean）
Vandermonde.lean（范德蒙行列式.lean）
Charpoly（特征多项式）
Trace.lean（迹.lean）
- 线性映射与线性空间
LinearIndependent.lean（线性无关.lean）
LinearDisjoint.lean（线性无关.lean）
LinearPMap.lean（线性投影映射.lean）
Isomorphisms.lean（同构.lean）
Quotient（商）
AffineSpace（仿射空间）
- 双线性形式与二次型
BilinearForm（双线性形式）
BilinearMap.lean（双线性映射.lean）
QuadraticForm（二次型）
SesquilinearForm.lean（半双线性型.lean）
- 特征值与特征空间
Eigenspace（特征空间）
AnnihilatingPolynomial.lean（零化多项式.lean）
JordanChevalley.lean（约当-舍瓦莱.lean）
- 张量积与外代数
TensorProduct（张量积）
TensorAlgebra（张量代数）
TensorPower（张量幂）
ExteriorAlgebra（外代数）
ExteriorPower（外幂）
PiTensorProduct.lean（π张量积.lean）
- 群与表示
GeneralLinearGroup.lean（一般线性群.lean）
SymplecticGroup.lean（辛群.lean）
UnitaryGroup.lean（酉群.lean）
RootSystem（根系）
Reflection.lean（反射.lean）
- 特殊结构与定理
Alternating（交错）
CliffordAlgebra（克利福德代数）
DirectSum（直和）
FreeModule（自由模）
FreeAlgebra.lean（自由代数.lean）
FreeProduct（自由积）
InvariantBasisNumber.lean（不变基数.lean）
PID.lean（主理想整环.lean）
Semisimple.lean（半单.lean）
- 几何与投影
Projectivization（射影化）
Projection.lean（投影.lean）
Orientation.lean（定向.lean）
Ray.lean（射线.lean）
- 其他工具与辅助模块
DFinsupp.lean（有限支撑函数.lean）
Finsupp（有限支撑）
Pi.lean（π.lean）
Prod.lean（积.lean）
Countable.lean（可数.lean）
Goursat.lean（古尔萨.lean）
Lagrange.lean（拉格朗日.lean）
PerfectPairing（完美配对）
SModEq.lean（模同余.lean）
Coevaluation.lean（余评估.lean）
Contraction.lean（收缩.lean）
CrossProduct.lean（叉积.lean）