Theorems · Theorem · number theory

NumberField.FinitePlace.hasFiniteMulSupport_fun_pow_multiplicity

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {M : Type u_3} [inst_2 : CommMonoid M]
  {I : Ideal (NumberField.RingOfIntegers K)},
  I ≠ ⊥ →
    ∀ (f : Ideal (NumberField.RingOfIntegers K) → M),
      Function.HasFiniteMulSupport fun v => f v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal I

Defined in

Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Cited by

0 results in Mathlib

Foundations

Depth 195 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberFieldCommMonoid