Documentation Verification Report

ValuationExactSequence

📁 Source: ClassFieldTheory/IsNonarchimedeanLocalField/ValuationExactSequence.lean

Statistics

Metric	Count
Definitions `repUnitsInteger`, `valuationShortComplex`, `units`	3
Theorems `repUnitsInteger_V_carrier`, `repUnitsInteger_V_isAddCommGroup_zsmul`, `repUnitsInteger_V_isModule_smul`, `val_inv_repUnitsInteger_V_isAddCommGroup_add_coe`, `val_inv_repUnitsInteger_V_isAddCommGroup_neg`, `val_inv_repUnitsInteger_V_isAddCommGroup_nsmul_coe`, `val_inv_repUnitsInteger_V_isAddCommGroup_sub_coe`, `val_inv_repUnitsInteger_V_isAddCommGroup_zero_coe`, `val_inv_repUnitsInteger_ρ_apply_hom_apply_coe`, `val_repUnitsInteger_V_isAddCommGroup_add_coe`, `val_repUnitsInteger_V_isAddCommGroup_neg`, `val_repUnitsInteger_V_isAddCommGroup_nsmul_coe`, `val_repUnitsInteger_V_isAddCommGroup_sub_coe`, `val_repUnitsInteger_V_isAddCommGroup_zero_coe`, `val_repUnitsInteger_ρ_apply_hom_apply_coe`, `shortExact`	16
Total	19

IsNonarchimedeanLocalField

Definitions

Name	Category	Theorems
`repUnitsInteger` 📖	CompOp	16 math math: `repUnitsInteger_V_carrier`, `val_inv_repUnitsInteger_V_isAddCommGroup_zero_coe`, `Rep.herbrandQuotient_isNonarchimedeanLocalField_integer_units`, `val_repUnitsInteger_V_isAddCommGroup_sub_coe`, `repUnitsInteger_V_isAddCommGroup_zsmul`, `repUnitsInteger_V_isModule_smul`, `val_repUnitsInteger_V_isAddCommGroup_neg`, `val_repUnitsInteger_V_isAddCommGroup_nsmul_coe`, `val_inv_repUnitsInteger_V_isAddCommGroup_sub_coe`, `val_inv_repUnitsInteger_V_isAddCommGroup_neg`, `val_inv_repUnitsInteger_ρ_apply_hom_apply_coe`, `val_repUnitsInteger_V_isAddCommGroup_add_coe`, `val_inv_repUnitsInteger_V_isAddCommGroup_add_coe`, `val_inv_repUnitsInteger_V_isAddCommGroup_nsmul_coe`, `val_repUnitsInteger_ρ_apply_hom_apply_coe`, `val_repUnitsInteger_V_isAddCommGroup_zero_coe`
`valuationShortComplex` 📖	CompOp	1 math math: `valuationShortComplex.shortExact`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`repUnitsInteger_V_carrier` 📖	mathematical	—	`repUnitsInteger`	—	—
`repUnitsInteger_V_isAddCommGroup_zsmul` 📖	mathematical	—	`repUnitsInteger`	—	—
`repUnitsInteger_V_isModule_smul` 📖	mathematical	—	`repUnitsInteger`	—	—
`val_inv_repUnitsInteger_V_isAddCommGroup_add_coe` 📖	mathematical	—	`repUnitsInteger`	—	`Units.coe_inv₀`
`val_inv_repUnitsInteger_V_isAddCommGroup_neg` 📖	mathematical	—	`repUnitsInteger`	—	—
`val_inv_repUnitsInteger_V_isAddCommGroup_nsmul_coe` 📖	mathematical	—	`repUnitsInteger`	—	`Units.coe_inv₀`
`val_inv_repUnitsInteger_V_isAddCommGroup_sub_coe` 📖	mathematical	—	`repUnitsInteger`	—	`Units.coe_inv₀`
`val_inv_repUnitsInteger_V_isAddCommGroup_zero_coe` 📖	mathematical	—	`repUnitsInteger`	—	—
`val_inv_repUnitsInteger_ρ_apply_hom_apply_coe` 📖	mathematical	—	`repUnitsInteger`	—	`Units.coe_inv₀`
`val_repUnitsInteger_V_isAddCommGroup_add_coe` 📖	mathematical	—	`repUnitsInteger`	—	—
`val_repUnitsInteger_V_isAddCommGroup_neg` 📖	mathematical	—	`repUnitsInteger`	—	—
`val_repUnitsInteger_V_isAddCommGroup_nsmul_coe` 📖	mathematical	—	`repUnitsInteger`	—	—
`val_repUnitsInteger_V_isAddCommGroup_sub_coe` 📖	mathematical	—	`repUnitsInteger`	—	`Units.coe_inv₀`
`val_repUnitsInteger_V_isAddCommGroup_zero_coe` 📖	mathematical	—	`repUnitsInteger`	—	—
`val_repUnitsInteger_ρ_apply_hom_apply_coe` 📖	mathematical	—	`repUnitsInteger`	—	—

IsNonarchimedeanLocalField.valuationShortComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`shortExact` 📖	mathematical	—	`IsNonarchimedeanLocalField.valuationShortComplex`	—	`CategoryTheory.ShortComplex.ShortExact.rep_exact_iff_function_exact` `IsNonarchimedeanLocalField.exact_kerV_v` `ValuativeRel.kerV_injective` `IsNonarchimedeanLocalField.v_surjective`

Rep

Definitions

Name	Category	Theorems
`units` 📖	CompOp	1 math math: `IsNonarchimedeanLocalField.instSubsingletonCarrierIntGroupCohomologyAlgEquivUnitsSubtypeMemSubringIntegerValueGroupWithZeroValuationOfIsUnramifiedOfNeZeroNat`

---

← Back to Index