Theorems · Definition · number theory

WeakFEPair.toStrongFEPair

{E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℂ E] → WeakFEPair E → WeakFEPair E

Given a weak FE-pair (f, g), modify it into a strong FE-pair by subtracting suitable correction terms from f and g. (See WeakFEPair.isStrongFEPair_toStrongFEPair for the proof that this is actually a strong FE-pair.)

Defined in

Mathlib.NumberTheory.LSeries.AbstractFuncEq

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace