NumberField

📁 Source: FLT/QuaternionAlgebra/NumberField.lean

Statistics

Metric	Count
Definitions restrictedProduct, toAdicCompletion, toAdicCompletion, localFullLevel, localTameLevel, TameLevel, TameLevel, localFullLevel, IsUnramified, Rigidification	10
Theorems isCompact, isOpen, isCompact, isOpen, mem_localFullLevel, mem_localFullLevel', mem_localFullLevel_iff_v_le_one_and_v_det_eq_one, v_det_val_mem_localFullLevel_eq_one, v_le_one_of_mem_localFullLevel, isCompact, isOpen, continuous_invFun, continuous_toFun, isCompact, isOpen	15
Total	25
⚠️ With sorry isCompact, isOpen, isCompact, isOpen, isCompact, isOpen	6

IsDedekindDomain.FiniteAdeleRing

Definitions

Name	Category	Theorems
toAdicCompletion 📖	CompOp	—

IsDedekindDomain.FiniteAdeleRing.GL2

Definitions

Name	Category	Theorems
restrictedProduct 📖	CompOp	—
toAdicCompletion 📖	CompOp	—

IsDedekindDomain.GL2

Definitions

Name	Category	Theorems
localFullLevel 📖	CompOp	3 math math: mem_localFullLevel_iff_v_le_one_and_v_det_eq_one, localFullLevel.isOpen, localFullLevel.isCompact
localTameLevel 📖	CompOp	2 math math: localTameLevel.isOpen, localTameLevel.isCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_localFullLevel 📖	—	localFullLevel	—	—	—
mem_localFullLevel' 📖	—	localFullLevel	—	—	mem_localFullLevel
mem_localFullLevel_iff_v_le_one_and_v_det_eq_one 📖	mathematical	—	localFullLevel	—	v_le_one_of_mem_localFullLevel v_det_val_mem_localFullLevel_eq_one Valued.isUnit_valuationSubring_iff
v_det_val_mem_localFullLevel_eq_one 📖	—	localFullLevel	—	—	mem_localFullLevel Valued.isUnit_valuationSubring_iff
v_le_one_of_mem_localFullLevel 📖	—	localFullLevel	—	—	—

IsDedekindDomain.GL2.localFullLevel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact 📖 ⚠️	mathematical	—	IsDedekindDomain.GL2.localFullLevel	—	—
isOpen 📖 ⚠️	mathematical	—	IsDedekindDomain.GL2.localFullLevel	—	—

IsDedekindDomain.GL2.localTameLevel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact 📖 ⚠️	mathematical	—	IsDedekindDomain.GL2.localTameLevel	—	—
isOpen 📖 ⚠️	mathematical	—	IsDedekindDomain.GL2.localTameLevel	—	—

IsDedekindDomain.HeightOneSpectrum.GL2

Definitions

Name	Category	Theorems
TameLevel 📖	CompOp	2 math math: TameLevel.isOpen, TameLevel.isCompact

IsDedekindDomain.HeightOneSpectrum.GL2.TameLevel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact 📖 ⚠️	mathematical	—	IsDedekindDomain.HeightOneSpectrum.GL2.TameLevel	—	—
isOpen 📖 ⚠️	mathematical	—	IsDedekindDomain.HeightOneSpectrum.GL2.TameLevel	—	—

IsDedekindDomain.HeightOneSpectrum.QuaternionAlgebra

Definitions

Name	Category	Theorems
TameLevel 📖	CompOp	—

IsDedekindDomain.HeightOneSpectrum.Rigidification

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_invFun 📖	mathematical	—	TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT IsQuaternionAlgebra.instFinite TensorProduct.RightActions.instAlgebra_fLT	—	instIsModuleTopologyMatrixOfIsTopologicalRingOfFinite_fLT IsQuaternionAlgebra.instFinite TensorProduct.RightActions.instIsModuleTopology_fLT
continuous_toFun 📖	mathematical	—	TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT IsQuaternionAlgebra.instFinite IsQuaternionAlgebra.NumberField.Rigidification TensorProduct.RightActions.instAlgebra_fLT	—	IsQuaternionAlgebra.instFinite TensorProduct.RightActions.instIsModuleTopology_fLT

IsDedekindDomain.M2

Definitions

Name	Category	Theorems
localFullLevel 📖	CompOp	2 math math: localFullLevel.isCompact, localFullLevel.isOpen

IsDedekindDomain.M2.localFullLevel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact 📖	mathematical	—	IsDedekindDomain.M2.localFullLevel	—	NumberField.instCompactSpaceAdicCompletionIntegers
isOpen 📖	mathematical	—	IsDedekindDomain.M2.localFullLevel	—	NumberField.isOpenAdicCompletionIntegers

IsQuaternionAlgebra.NumberField

Definitions

Name	Category	Theorems
IsUnramified 📖	MathDef	—
Rigidification 📖	CompOp	1 math math: IsDedekindDomain.HeightOneSpectrum.Rigidification.continuous_toFun

---

← Back to Index