Documentation Verification Report

FiniteAdeleRing

📁 Source: FLT/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

Statistics

Metric	Count
Definitions `evalAlgebraMap`, `evalContinuousAlgebraMap`, `integralAdeles`, `localIdempotent`, `mk`, `singleContinuousLinearMap`, `singleLinearMap`, `singleMulHom`	8
Theorems `evalAlgebraMap_singleLinearMap`, `evalContinuousAlgebraMap_singleContinuousLinearMap`, `eval_localIdempotent`, `mk_apply`, `mul_apply`, `one_apply`, `singleContinuousAlgebraMap_comp_evalContinuousLinearMap`	7
Total	15

IsDedekindDomain.FiniteAdeleRing

Definitions

Name	Category	Theorems
`evalAlgebraMap` 📖	CompOp	1 math math: `evalAlgebraMap_singleLinearMap`
`evalContinuousAlgebraMap` 📖	CompOp	6 math math: `singleContinuousAlgebraMap_comp_evalContinuousLinearMap`, `localcomponent_mulLeft`, `localcomponent_mulRight`, `eval_localIdempotent`, `TensorProduct.localcomponent_apply`, `evalContinuousAlgebraMap_singleContinuousLinearMap`
`integralAdeles` 📖	CompOp	3 math math: `Rat.FiniteAdeleRing.padicEquiv_bijOn`, `Rat.FiniteAdeleRing.sub_mem_integralAdeles`, `instCompactSpaceSubtypeFiniteAdeleRingRingOfIntegersMemSubringIntegralAdeles`
`localIdempotent` 📖	CompOp	2 math math: `singleContinuousAlgebraMap_comp_evalContinuousLinearMap`, `eval_localIdempotent`
`mk` 📖	CompOp	—
`singleContinuousLinearMap` 📖	CompOp	2 math math: `singleContinuousAlgebraMap_comp_evalContinuousLinearMap`, `evalContinuousAlgebraMap_singleContinuousLinearMap`
`singleLinearMap` 📖	CompOp	1 math math: `evalAlgebraMap_singleLinearMap`
`singleMulHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`evalAlgebraMap_singleLinearMap` 📖	mathematical	—	`evalAlgebraMap` `singleLinearMap`	—	—
`evalContinuousAlgebraMap_singleContinuousLinearMap` 📖	mathematical	—	`evalContinuousAlgebraMap` `singleContinuousLinearMap`	—	—
`eval_localIdempotent` 📖	mathematical	—	`evalContinuousAlgebraMap` `localIdempotent`	—	—
`mk_apply` 📖	—	—	—	—	—
`mul_apply` 📖	—	—	—	—	—
`one_apply` 📖	—	—	—	—	—
`singleContinuousAlgebraMap_comp_evalContinuousLinearMap` 📖	mathematical	—	`singleContinuousLinearMap` `evalContinuousAlgebraMap` `localIdempotent`	—	—

---

← Back to Index