Theorem ContinuousMapZero.coe_neg

Modification history

2026-10-29 22:29

Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean

chore(Topology): use `IsApply` for `ContinuousMapZero` (#45292)

Deleted ContinuousMapZero.coe_neg View on Github →

2025-06-20 15:07

Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean

feat: [Normed]AddCommGroup instance for ContinuousMapZero (#26079) …

Modified ContinuousMapZero.coe_neg View on Github →

2024-05-29 14:23

Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean

feat: add more features to `ContinuousMapZero` (#13323) …

Added ContinuousMapZero.coe_neg View on Github →