Theorem Irreducible.maximalIdeal_eq_closedBall

Modification history

2024-12-20 12:02

Mathlib/Topology/Algebra/Valued/LocallyCompact.lean

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

Added Irreducible.maximalIdeal_eq_closedBall View on Github →