Valuation

📁 Source: ClassFieldTheory/IsNonarchimedeanLocalField/Valuation.lean

Statistics

Metric	Count
Definitions v, valuationInt, kerV	3
Theorems exact_kerV_v, instCompatibleWithZeroMultiplicativeIntValuationInt, v_apply, v_eq_zero_iff, v_surjective, v_uniformiser, valuationInt_uniformiser, strict_mono, kerV_apply, kerV_injective, log_eq_zero_iff	11
Total	14

IsNonarchimedeanLocalField

Definitions

Name	Category	Theorems
v 📖	CompOp	5 math math: v_surjective, v_eq_zero_iff, v_apply, v_uniformiser, exact_kerV_v
valuationInt 📖	CompOp	3 math math: instCompatibleWithZeroMultiplicativeIntValuationInt, valuationInt_uniformiser, v_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exact_kerV_v 📖	mathematical	—	ValuativeRel.kerV v	—	v_eq_zero_iff valuation_eq_one_iff
instCompatibleWithZeroMultiplicativeIntValuationInt 📖	mathematical	—	valuationInt	—	Valuation.compatible_map OrderIsoClass.strict_mono
v_apply 📖	mathematical	—	v valuationInt	—	—
v_eq_zero_iff 📖	mathematical	—	v	—	v_apply instCompatibleWithZeroMultiplicativeIntValuationInt
v_surjective 📖	mathematical	—	v	—	Irreducible.ne_zero' v_apply valuationInt_uniformiser
v_uniformiser 📖	mathematical	—	v Irreducible.ne_zero'	—	Irreducible.ne_zero' v_apply valuationInt_uniformiser
valuationInt_uniformiser 📖	mathematical	—	valuationInt	—	valueGroupWithZeroIsoInt_irreducible

OrderIsoClass

Theorems

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

ValuativeRel

Definitions

Name	Category	Theorems
kerV 📖	CompOp	3 math math: kerV_apply, kerV_injective, IsNonarchimedeanLocalField.exact_kerV_v

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
kerV_apply 📖	mathematical	—	kerV	—	—
kerV_injective 📖	mathematical	—	kerV	—	—

WithZero

Theorems

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

---

← Back to Index