LocalUnits

📁 Source: FLT/DedekindDomain/FiniteAdeleRing/LocalUnits.lean

Statistics

Metric	Count
Definitions localUniformiser, localUniformiserUnit, localUnit, adicCompletionIntegersUniformizer, adicCompletionUniformizer, adicCompletionUniformizerUnit	6
Theorems localUniformiser_eval, localUnit_eval_of_eq, localUnit_eval_of_ne, adicCompletionUniformizer_ne_zero, adicCompletionUniformizer_spec	5
Total	11

IsDedekindDomain.FiniteAdeleRing

Definitions

Name	Category	Theorems
localUniformiser 📖	CompOp	1 math math: localUniformiser_eval
localUniformiserUnit 📖	CompOp	—
localUnit 📖	CompOp	2 math math: localUnit_eval_of_eq, localUnit_eval_of_ne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
localUniformiser_eval 📖	mathematical	—	localUniformiser IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizer	—	—
localUnit_eval_of_eq 📖	mathematical	—	localUnit	—	—
localUnit_eval_of_ne 📖	mathematical	—	localUnit	—	—

IsDedekindDomain.HeightOneSpectrum

Definitions

Name	Category	Theorems
adicCompletionIntegersUniformizer 📖	CompOp	—
adicCompletionUniformizer 📖	CompOp	2 math math: IsDedekindDomain.FiniteAdeleRing.localUniformiser_eval, adicCompletionUniformizer_spec
adicCompletionUniformizerUnit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adicCompletionUniformizer_ne_zero 📖	—	—	—	—	adicCompletionUniformizer_spec
adicCompletionUniformizer_spec 📖	mathematical	—	adicCompletionUniformizer	—	—

---

← Back to Index