ValuativeRel

📁 Source: ClassFieldTheory/Mathlib/RingTheory/Valuation/ValuativeRel.lean

Statistics

Metric	Count
Definitions instSubtypeMem_classFieldTheory	1
Theorems compatible_map, algebraMap_eq, algebraMap_le, algebraMap_lt, inst_classFieldTheory, trans, ext_of_field, ext_of_field_iff, instValuativeExtensionSubtypeMem_classFieldTheory, instValuativeExtensionSubtypeMem_classFieldTheory_1, ne_zero, subringclassRel_eq, subringclassRel_iff, unitsMap_valuation_surjective, vle_iff_div_vle_one	15
Total	16

Valuation

Theorems

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

ValuativeExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_eq 📖	—	—	—	—	—
algebraMap_le 📖	—	—	—	—	—
algebraMap_lt 📖	—	—	—	—	—
inst_classFieldTheory 📖	—	—	—	—	—
trans 📖	—	—	—	—	—

ValuativeRel

Definitions

Name	Category	Theorems
instSubtypeMem_classFieldTheory 📖	CompOp	11 math math: subringclassRel_iff, IsNonarchimedeanLocalField.instSubtypeMemIntermediateField_classFieldTheory, subringclassRel_eq, IsNonarchimedeanLocalField.e_fieldRange, instValuativeExtensionSubtypeMem_classFieldTheory, instValuativeExtensionSubtypeMem_classFieldTheory_1, IsNonarchimedeanLocalField.le_maximalUnramified_iff, IsNonarchimedeanLocalField.instIsUnramifiedSubtypeMemIntermediateFieldMaximalUnramified, IsNonarchimedeanLocalField.instIsUnramifiedSubtypeMemIntermediateFieldFieldRange, IsNonarchimedeanLocalField.f_fieldRange, IsNonarchimedeanLocalField.InUnramified.intermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_of_field 📖	—	—	—	—	vle_iff_div_vle_one
ext_of_field_iff 📖	—	—	—	—	ext_of_field
instValuativeExtensionSubtypeMem_classFieldTheory 📖	mathematical	—	instSubtypeMem_classFieldTheory	—	—
instValuativeExtensionSubtypeMem_classFieldTheory_1 📖	mathematical	—	instSubtypeMem_classFieldTheory	—	—
subringclassRel_eq 📖	mathematical	—	instSubtypeMem_classFieldTheory	—	—
subringclassRel_iff 📖	mathematical	—	instSubtypeMem_classFieldTheory	—	—
unitsMap_valuation_surjective 📖	—	—	—	—	—
vle_iff_div_vle_one 📖	—	—	—	—	—

ValuativeRel.posSubmonoid

Theorems

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

---

← Back to Index