Theorem ZeroAtInftyContinuousMap.toOnePoint_smul

Modification history

2026-09-29 22:08
Mathlib/Topology/ContinuousMap/ZeroAtInftyUnitization.lean
feat: generalize SMul instances from DistribMulAction to DistribSMul (#41736) …
Modified ZeroAtInftyContinuousMap.toOnePoint_smulView on Github →
2026-08-21 02:09
Mathlib/Topology/ContinuousMap/ZeroAtInftyUnitization.lean
feat: `Unitization R C₀(X, R) ≃ C(OnePoint X, R)` (#42934) …
Added ZeroAtInftyContinuousMap.toOnePoint_smulView on Github →