Commit 2026-01-28 18:47 087469e2

View on Github →

chore(Analysis/LocallyConvex/SeparatingDual): generalize Algebra.IsCentral.instContinuousLinearMap (#33351) ... to two different scalar fields.

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/SeparatingDual.lean

modified theorem SeparatingDual.exists_continuousLinearEquiv_apply_eq

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

modified theorem ContinuousLinearMap.algebraMap_apply

added theorem ContinuousLinearMap.toSpanSingleton_comp