Documentation Verification Report

Equiv

📁 Source: FLT/Mathlib/Topology/Algebra/Module/Equiv.lean

Statistics

Metric	Count
Definitions `piScalarPiComm`, `piScalarPiCongrFiberwise`, `restrictScalars`, `toContinuousAddEquiv`, `toContinuousLinearEquiv`	5
Theorems `restrictScalars_apply`, `restrictScalars_symm_apply`, `toContinuousAddEquiv_trans`, `toMatrix_det_ne_zero`, `toMatrix_isUnit`, `toMatrix_isUnit_det`, `toMatrix_toContinousLinearEquiv`, `toContinousLinearEquiv_apply`, `toContinousLinearEquiv_mul`, `toContinousLinearEquiv_toMatrix`, `toContinuousLinearEquiv_toLin_coe`, `toContinuousLinearEquiv_toLinearEquiv`	12
Total	17

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
`piScalarPiComm` 📖	CompOp	—
`piScalarPiCongrFiberwise` 📖	CompOp	—
`restrictScalars` 📖	CompOp	2 math math: `restrictScalars_symm_apply`, `restrictScalars_apply`
`toContinuousAddEquiv` 📖	CompOp	15 math math: `FiniteAdeleRing.Aux.g_commSq`, `MeasureTheory.addHaarScalarFactor_tensor_adeles_eq_one`, `localcomponent_mulLeft`, `localcomponent_mulRight`, `MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc`, `MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_pi`, `basis_eq`, `MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det`, `MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_diagonal`, `MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_matrix_pi`, `MeasureTheory.addHaarScalarFactor_tensor_adeles_rat_eq_one`, `toContinuousAddEquiv_trans`, `FiniteAdeleRing.Aux.f_commSq`, `basis_eq_global`, `FiniteAdeleRing.Aux.e_commSq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictScalars_apply` 📖	mathematical	—	`restrictScalars`	—	—
`restrictScalars_symm_apply` 📖	mathematical	—	`restrictScalars`	—	—
`toContinuousAddEquiv_trans` 📖	mathematical	—	`toContinuousAddEquiv`	—	—
`toMatrix_det_ne_zero` 📖	—	—	—	—	`toMatrix_isUnit_det`
`toMatrix_isUnit` 📖	—	—	—	—	`toMatrix_isUnit_det`
`toMatrix_isUnit_det` 📖	—	—	—	—	—
`toMatrix_toContinousLinearEquiv` 📖	mathematical	—	`Matrix.toContinuousLinearEquiv` `toMatrix_isUnit_det`	—	`toMatrix_isUnit_det`

Matrix

Definitions

Name	Category	Theorems
`toContinuousLinearEquiv` 📖	CompOp	7 math math: `ContinuousLinearEquiv.toMatrix_toContinousLinearEquiv`, `toContinousLinearEquiv_toMatrix`, `toContinuousLinearEquiv_toLinearEquiv`, `toContinuousLinearEquiv_toLin_coe`, `toContinousLinearEquiv_apply`, `MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_matrix_pi`, `toContinousLinearEquiv_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toContinousLinearEquiv_apply` 📖	mathematical	—	`toContinuousLinearEquiv`	—	—
`toContinousLinearEquiv_mul` 📖	mathematical	—	`toContinuousLinearEquiv`	—	—
`toContinousLinearEquiv_toMatrix` 📖	mathematical	—	`toContinuousLinearEquiv`	—	—
`toContinuousLinearEquiv_toLin_coe` 📖	mathematical	—	`toContinuousLinearEquiv`	—	—
`toContinuousLinearEquiv_toLinearEquiv` 📖	mathematical	—	`toContinuousLinearEquiv`	—	—

---

← Back to Index