Commit 2024-09-17 11:41 610ec983

View on Github →

chore: split Topology.Algebra.Module.WeakDual (#16489)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

Modified Mathlib/Analysis/LocallyConvex/Polar.lean

Modified Mathlib/Analysis/LocallyConvex/WeakDual.lean

Modified Mathlib/Analysis/Normed/Module/WeakDual.lean

Created Mathlib/Topology/Algebra/Module/WeakBilin.lean

added theorem WeakBilin.coeFn_continuous

added theorem WeakBilin.continuous_of_continuous_eval

added theorem WeakBilin.embedding

added theorem WeakBilin.eval_continuous

added theorem WeakBilin.tendsto_iff_forall_eval_tendsto

added def WeakBilin

Modified Mathlib/Topology/Algebra/Module/WeakDual.lean

deleted theorem WeakBilin.coeFn_continuous

deleted theorem WeakBilin.continuous_of_continuous_eval

deleted theorem WeakBilin.embedding

deleted theorem WeakBilin.eval_continuous

deleted theorem WeakBilin.tendsto_iff_forall_eval_tendsto

deleted def WeakBilin