Documentation Verification Report

Matrix

📁 Source: Mathlib/GroupTheory/Coxeter/Matrix.lean

Statistics

Metric	Count
Definitions `CoxeterMatrix`, `Aₙ`, `Bₙ`, `Dₙ`, `E₆`, `E₇`, `E₈`, `F₄`, `G₂`, `H₃`, `H₄`, `I₂ₘ`, `instCoeFunMatrixNat`, `reindex`	14
Theorems `diagonal`, `ext`, `ext_iff`, `isSymm`, `off_diagonal`, `reindex_apply`, `symmetric`	7
Total	21

CoxeterMatrix

Definitions

Name	Category	Theorems
`Aₙ` 📖	CompOp	—
`Bₙ` 📖	CompOp	—
`Dₙ` 📖	CompOp	—
`E₆` 📖	CompOp	—
`E₇` 📖	CompOp	—
`E₈` 📖	CompOp	—
`F₄` 📖	CompOp	—
`G₂` 📖	CompOp	—
`H₃` 📖	CompOp	—
`H₄` 📖	CompOp	—
`I₂ₘ` 📖	CompOp	—
`instCoeFunMatrixNat` 📖	CompOp	—
`reindex` 📖	CompOp	6 math math: `CoxeterSystem.reindex_mulEquiv`, `reindex_relationsSet`, `reindexGroupEquiv_apply_simple`, `reindex_apply`, `CoxeterSystem.reindex_simple`, `reindexGroupEquiv_symm_apply_simple`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diagonal` 📖	mathematical	—	`M`	—	—
`ext` 📖	—	`M`	—	—	—
`ext_iff` 📖	mathematical	—	`M`	—	`ext`
`isSymm` 📖	mathematical	—	`Matrix.IsSymm` `M`	—	—
`off_diagonal` 📖	—	—	—	—	—
`reindex_apply` 📖	mathematical	—	`M` `reindex` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—
`symmetric` 📖	mathematical	—	`M`	—	`Matrix.IsSymm.apply` `isSymm`

(root)

Definitions

Name	Category	Theorems
`CoxeterMatrix` 📖	CompData	—

---

← Back to Index