Theorems · Definition · field theory

Valued.maximalIdeal

(K : Type u_1) →
  [inst : Field K] →
    {Γ₀ : outParam (Type u_2)} →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → [vK : Valued K Γ₀] → Ideal ↥(Valued.integer K)

An abbreviation for IsLocalRing.maximalIdeal 𝒪[K] of a valued field K, enabling the notation 𝓂[K] for the maximal ideal in 𝒪[K] of a valued field K.

Defined in: Mathlib.Topology.Algebra.Valued.ValuedField
Cited by: 4 results in Mathlib
Foundations: Depth 53 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field LinearOrderedCommGroupWithZero Valued

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Fieldstatement and proof · cited by 7,404
Idealstatement · cited by 4,748
Subringstatement · cited by 602
LinearOrderedCommGroupWithZerostatement and proof · cited by 528
IsLocalRing.maximalIdealproof · cited by 297
Valuedstatement and proof · cited by 70
Valued.integerstatement and proof · cited by 22

Cited by4

Results whose statement or proof uses this declaration.

Valued.integer.totallyBounded_iff_finite_residueFieldproof · cited by 1
Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueFieldstatement and proof · cited by 1
Irreducible.maximalIdeal_eq_closedBallstatement · cited by 0
Irreducible.maximalIdeal_pow_eq_closedBall_powstatement · cited by 0