Theorem Valued.integer.totallyBounded_iff_finite_residueField

Modification history

2025-07-14 06:20

Mathlib/Topology/Algebra/Valued/LocallyCompact.lean

feat(Valued/LocallyCompact): locally compact iff complete and DVR and finite residue field (#26549) …

Modified Valued.integer.totallyBounded_iff_finite_residueField View on Github →

2024-12-20 12:02

Mathlib/Topology/Algebra/Valued/LocallyCompact.lean

feat(Valued/LocallyCompact): `totallyBounded_iff_finite_residueField` (#15424)

Added Valued.integer.totallyBounded_iff_finite_residueField View on Github →