Theorem Irreducible.maximalIdeal_pow_eq_closedBall_pow

Modification history

2024-12-20 12:02
Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
feat(Valued/LocallyCompact): `totallyBounded_iff_finite_residueField` (#15424)
Added Irreducible.maximalIdeal_pow_eq_closedBall_powView on Github →