FiniteDimensional

📁 Source: FLT/HaarMeasure/HaarChar/FiniteDimensional.lean

Statistics

Metric	Count
Definitions mulLeft, mulRight	2
Theorems ringHaarChar_eq_addEquivAddHaarChar_mulRight, measurePreserving, addEquivAddHaarChar_eq_ringHaarChar_det, addEquivAddHaarChar_eq_ringHaarChar_det_diagonal, addEquivAddHaarChar_eq_ringHaarChar_det_matrix_pi, addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc, addEquivAddHaarChar_eq_ringHaarChar_det_pi, algebra_ringHaarChar_eq_ringHaarChar_det	8
Total	10

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
mulLeft 📖	CompOp	1 math math: localcomponent_mulLeft
mulRight 📖	CompOp	1 math math: localcomponent_mulRight

IsSimpleRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ringHaarChar_eq_addEquivAddHaarChar_mulRight 📖	mathematical	—	MeasureTheory.ringHaarChar ContinuousAddEquiv.mulRight	—	MeasureTheory.algebra_ringHaarChar_eq_ringHaarChar_det mulLeft_det_eq_mulRight_det' MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addEquivAddHaarChar_eq_ringHaarChar_det 📖	mathematical	—	ContinuousLinearEquiv.toContinuousAddEquiv ringHaarChar	—	addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec'
addEquivAddHaarChar_eq_ringHaarChar_det_diagonal 📖	mathematical	—	ContinuousLinearEquiv.toContinuousAddEquiv ringHaarChar	—	addEquivAddHaarChar_piCongrRight
addEquivAddHaarChar_eq_ringHaarChar_det_matrix_pi 📖	mathematical	Matrix.Pivot.ExistsListTransvecMulDiagonalMulListTransvec	ContinuousLinearEquiv.toContinuousAddEquiv Matrix.toContinuousLinearEquiv ringHaarChar	—	Matrix.diagonal_transvection_induction_of_det_unit Matrix.toContinousLinearEquiv_toMatrix addEquivAddHaarChar_eq_ringHaarChar_det_diagonal Matrix.TransvectionStruct.measurePreserving LinearEquiv.det_toLinearEquiv Matrix.toContinousLinearEquiv_mul
addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc 📖	mathematical	Matrix.Pivot.ExistsListTransvecMulDiagonalMulListTransvec	ContinuousLinearEquiv.toContinuousAddEquiv ringHaarChar	—	addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv addEquivAddHaarChar_eq_ringHaarChar_det_pi
addEquivAddHaarChar_eq_ringHaarChar_det_pi 📖	mathematical	Matrix.Pivot.ExistsListTransvecMulDiagonalMulListTransvec	ContinuousLinearEquiv.toContinuousAddEquiv ringHaarChar	—	ContinuousLinearEquiv.toMatrix_isUnit_det ContinuousLinearEquiv.toMatrix_toContinousLinearEquiv addEquivAddHaarChar_eq_ringHaarChar_det_matrix_pi
algebra_ringHaarChar_eq_ringHaarChar_det 📖	mathematical	—	ringHaarChar LinearEquiv.mulLeft	—	addEquivAddHaarChar_eq_ringHaarChar_det

MeasureTheory.Matrix.TransvectionStruct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurePreserving 📖	—	—	—	—	—

---

← Back to Index