Theorem Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueField

Modification history

2026-08-27 00:26
Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
feat(LocalRing): instance `Finite (R / maximalIdeal R ^ n)` (#42994) …
Deleted Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueFieldView on Github →
2024-12-20 12:02
Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
feat(Valued/LocallyCompact): `totallyBounded_iff_finite_residueField` (#15424)
Added Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueFieldView on Github →