Theorems · Theorem · number theory

WeakFEPair.h_feq

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (self : WeakFEPair E),
  ∀ x ∈ Set.Ioi 0, self.f (1 / x) = (self.ε * ↑(x ^ self.k)) • self.g x

Defined in

Mathlib.NumberTheory.LSeries.AbstractFuncEq

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace