WithZeroMulInt

Statistics

Metric	Count
Definitions	0
Theorems `exists_pow_lt_of_le_neg_one`, `finite_cover_of_uniformity_basis`, `finite_quotient_maximalIdeal_pow_of_finite_residueField`, `integer_compactSpace`, `irreducible_valuation_le_ofAdd_neg_one`, `irreducible_valuation_lt_one`, `mem_maximalIdeal_pow_valuation`, `tendsto_zero_pow_of_le_neg_one`	8
Total	8

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_pow_lt_of_le_neg_one` 📖	—	—	—	—	`tendsto_zero_pow_of_le_neg_one`
`finite_cover_of_uniformity_basis` 📖	—	—	—	—	`exists_pow_lt_of_le_neg_one` `irreducible_valuation_le_ofAdd_neg_one` `finite_quotient_maximalIdeal_pow_of_finite_residueField` `mem_maximalIdeal_pow_valuation` `Ideal.Quotient.out_sub`
`finite_quotient_maximalIdeal_pow_of_finite_residueField` 📖	—	—	—	—	—
`integer_compactSpace` 📖	—	—	—	—	`finite_cover_of_uniformity_basis`
`irreducible_valuation_le_ofAdd_neg_one` 📖	—	—	—	—	—
`irreducible_valuation_lt_one` 📖	—	—	—	—	—
`mem_maximalIdeal_pow_valuation` 📖	—	—	—	—	—
`tendsto_zero_pow_of_le_neg_one` 📖	—	—	—	—	—

---