Theorem ContinuousLinearMap.coe_one

Modification history

2026-06-10 03:47

Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean

feat(Topology/Algebra): use `Is*Apply` for `ContinuousLinearMap` (#39637) …

Deleted ContinuousLinearMap.coe_one View on Github →

2026-03-03 16:04

Mathlib/Topology/Algebra/Module/LinearMap.lean

refactor(Topology/Algebra/Module/LinearMap): adjust statement of `coe_mul` and `coe_pow` (#35269) …

Added ContinuousLinearMap.coe_one View on Github →