Commit 2024-12-20 12:02 e5485b24

View on Github →

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

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Valuation/Integers.lean

added theorem Valuation.Integers.valuation_unit

Created Mathlib/Topology/Algebra/Valued/LocallyCompact.lean

added theorem Irreducible.maximalIdeal_eq_closedBall

added theorem Irreducible.maximalIdeal_pow_eq_closedBall_pow

added theorem NormedField.v_eq_valuation

added theorem Valued.integer.coe_span_singleton_eq_closedBall

added theorem Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueField

added theorem Valued.integer.isUnit_iff_norm_eq_one

added theorem Valued.integer.mem_iff

added theorem Valued.integer.norm_coe_unit

added theorem Valued.integer.norm_irreducible_lt_one

added theorem Valued.integer.norm_irreducible_pos

added theorem Valued.integer.norm_le_one

added theorem Valued.integer.norm_unit

added theorem Valued.integer.totallyBounded_iff_finite_residueField