HerbrandQuotient

Statistics

Metric	Count
Definitions	0
Theorems `herbrandQuotient_isNonarchimedeanLocalField_integer_units`, `herbrandQuotient_isNonarchimedeanLocalField_units`	2
Total	2
⚠️ With sorry `herbrandQuotient_isNonarchimedeanLocalField_integer_units`	1

Name	Kind	Assumes	Proves	Validates	Depends On
`herbrandQuotient_isNonarchimedeanLocalField_integer_units` 📖 ⚠️	mathematical	—	`herbrandQuotient` `IsNonarchimedeanLocalField.repUnitsInteger`	—	—
`herbrandQuotient_isNonarchimedeanLocalField_units` 📖	mathematical	—	`herbrandQuotient` `res`	—	`herbrandQuotient_isNonarchimedeanLocalField_integer_units` `herbrandQuotient_trivial_int_eq_card` `herbrandQuotient_eq_of_shortExact` `IsNonarchimedeanLocalField.valuationShortComplex.shortExact` `herbrandQuotient_ne_zero_of_shortExact₂`

---