Theorem PontryaginDual.map_one

Modification history

2025-03-14 13:35
Mathlib/Topology/Algebra/PontryaginDual.lean
feat(ContinuousMonoidHom): add notation for ContinuousMonoidHom and ContinuousAddMonoidHom (#21300) …
Modified PontryaginDual.map_oneView on Github →
2025-02-11 16:20
Mathlib/Topology/Algebra/PontryaginDual.lean
feat: lemmas about forgetting linearity of ContinuousLinearMap (#21444)
Modified PontryaginDual.map_oneView on Github →
2024-02-20 23:51
Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
refactor: Split off the Pontryagin dual into separate file (#10620) …
Modified PontryaginDual.map_oneView on Github →
2023-05-30 08:46
Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
feat: port Topology.Algebra.ContinuousMonoidHom (#4162)
Added PontryaginDual.map_oneView on Github →