Theorem ContinuousMapZero.coe_sum

Modification history

2026-10-29 22:29

Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean

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

Modified ContinuousMapZero.coe_sum View on Github →

2024-06-23 01:13

Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean

feat(ContinuousFunctionalCalculus): add lemmas about the CFC applied to finite sums (#13842)

Added ContinuousMapZero.coe_sum View on Github →