Documentation Verification Report

Ring

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

Statistics

Metric	Count
Definitions `mulLeft`, `mulRight`, `ringHaarChar`, `ringHaarChar_ker`	4
Theorems `mulLeft_apply`, `mulRight_apply`, `preimage_mulLeft_smul`, `mem_ringHaarChar_ker`, `ringHaarChar_ModuleFinite`, `ringHaarChar_ModuleFinite_unit`, `ringHaarChar_apply`, `ringHaarChar_continuous`, `ringHaarChar_eq_of_measure_smul_eq_mul`, `ringHaarChar_eq_ringHaarChar_of_continuousAlgEquiv`, `ringHaarChar_mul_integral`, `ringHaarChar_mul_volume`, `ringHaarChar_pi`, `ringHaarChar_pi'`, `ringHaarChar_prod`, `ringHaarChar_prod'`, `ringHaarChar_restrictedProduct`, `ringHaarChar_toFun`	18
Total	22

ContinuousAddEquiv

Definitions

Name	Category	Theorems
`mulLeft` 📖	CompOp	11 math math: `MeasureTheory.ringHaarChar_apply`, `preimage_mulLeft_smul`, `localcomponent_mulLeft`, `NumberField.InfiniteAdeleRing.isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul`, `NumberField.FiniteAdeleRing.tensor_isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul`, `NumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul`, `mulLeft_apply`, `NumberField.FiniteAdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul`, `NumberField.InfiniteAdeleRing.isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul_aux`, `MeasureTheory.ringHaarChar_continuous`, `MeasureTheory.ringHaarChar_toFun`
`mulRight` 📖	CompOp	9 math math: `IsSimpleRing.ringHaarChar_eq_addEquivAddHaarChar_mulRight`, `localcomponent_mulRight`, `mulRight_apply`, `NumberField.InfiniteAdeleRing.isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul`, `NumberField.FiniteAdeleRing.tensor_isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul`, `NumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul`, `NumberField.AdeleRing.addEquivAddHaarChar_mulRight_unit_eq_one`, `NumberField.FiniteAdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul`, `NumberField.InfiniteAdeleRing.isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul_aux`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulLeft_apply` 📖	mathematical	—	`mulLeft`	—	—
`mulRight_apply` 📖	mathematical	—	`mulRight`	—	—
`preimage_mulLeft_smul` 📖	mathematical	—	`mulLeft`	—	—

MeasureTheory

Definitions

Name	Category	Theorems
`ringHaarChar` 📖	CompOp	30 math math: `ringHaarChar_apply`, `ringHaarChar_prod`, `IsSimpleRing.ringHaarChar_eq_addEquivAddHaarChar_mulRight`, `mem_ringHaarChar_ker`, `ringHaarChar_restrictedProduct`, `ringHaarChar_adeles_rat`, `NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸`, `addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc`, `ringHaarChar_eq_of_measure_smul_eq_mul`, `addEquivAddHaarChar_eq_ringHaarChar_det_pi`, `ringHaarChar_pi`, `ringHaarChar_ModuleFinite`, `ringHaarChar_pi'`, `ringHaarChar_complex`, `addEquivAddHaarChar_eq_ringHaarChar_det`, `addEquivAddHaarChar_eq_ringHaarChar_det_diagonal`, `ringHaarChar_real`, `addEquivAddHaarChar_eq_ringHaarChar_det_matrix_pi`, `ringHaarChar_adeles_units_rat_eq_one`, `NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸_prodRight_units_aux`, `ringHaarChar_padic`, `ringHaarChar_mul_integral`, `ringHaarChar_mul_volume`, `NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸_real_surjective`, `ringHaarChar_padicInt`, `ringHaarChar_ModuleFinite_unit`, `algebra_ringHaarChar_eq_ringHaarChar_det`, `ringHaarChar_prod'`, `ringHaarChar_toFun`, `ringHaarChar_eq_ringHaarChar_of_continuousAlgEquiv`
`ringHaarChar_ker` 📖	CompOp	11 math math: `mem_ringHaarChar_ker`, `NumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_surjective`, `NumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_continuous`, `NumberField.AdeleRing.DivisionAlgebra.Aux.toQuot_cont`, `NumberField.AdeleRing.units_mem_ringHaarCharacter_ker`, `NumberField.AdeleRing.DivisionAlgebra.Aux.toQuot_surjective`, `NumberField.AdeleRing.DivisionAlgebra.compact_quotient`, `NumberField.AdeleRing.DivisionAlgebra.Aux.rest₁_surjective`, `NumberField.AdeleRing.DivisionAlgebra.Aux.rest₁_continuous`, `NumberField.AdeleRing.DivisionAlgebra.Aux.M_compact`, `NumberField.AdeleRing.DivisionAlgebra.Aux.incl₂_isClosedEmbedding`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_ringHaarChar_ker` 📖	mathematical	—	`ringHaarChar_ker` `ringHaarChar`	—	—
`ringHaarChar_ModuleFinite` 📖	mathematical	—	`ringHaarChar`	—	`addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv`
`ringHaarChar_ModuleFinite_unit` 📖	mathematical	—	`ringHaarChar`	—	`ringHaarChar_ModuleFinite` `ringHaarChar_pi`
`ringHaarChar_apply` 📖	mathematical	—	`ringHaarChar` `ContinuousAddEquiv.mulLeft`	—	—
`ringHaarChar_continuous` 📖	mathematical	—	`ContinuousAddEquiv.mulLeft`	—	—
`ringHaarChar_eq_of_measure_smul_eq_mul` 📖	mathematical	—	`ringHaarChar`	—	`ringHaarChar_mul_volume`
`ringHaarChar_eq_ringHaarChar_of_continuousAlgEquiv` 📖	mathematical	—	`ringHaarChar`	—	`addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv`
`ringHaarChar_mul_integral` 📖	mathematical	—	`ringHaarChar`	—	—
`ringHaarChar_mul_volume` 📖	mathematical	—	`ringHaarChar`	—	`ringHaarChar_toFun` `ContinuousAddEquiv.preimage_mulLeft_smul`
`ringHaarChar_pi` 📖	mathematical	—	`ringHaarChar`	—	`addEquivAddHaarChar_piCongrRight`
`ringHaarChar_pi'` 📖	mathematical	—	`ringHaarChar`	—	`addEquivAddHaarChar_piCongrRight`
`ringHaarChar_prod` 📖	mathematical	—	`ringHaarChar`	—	`addEquivAddHaarChar_prodCongr`
`ringHaarChar_prod'` 📖	mathematical	—	`ringHaarChar`	—	`ringHaarChar_prod`
`ringHaarChar_restrictedProduct` 📖	mathematical	—	`ringHaarChar` `instMeasurableSpaceRestrictedProduct_fLT` `instBorelSpaceRestrictedProduct_fLT` `MulEquiv.restrictedProductUnits`	—	`instBorelSpaceRestrictedProduct_fLT` `addEquivAddHaarChar_restrictedProductCongrRight`
`ringHaarChar_toFun` 📖	mathematical	—	`ringHaarChar` `ContinuousAddEquiv.mulLeft`	—	—

---

← Back to Index