Theorem ContinuousMap.coe_inv

Modification history

2024-01-16 00:56

Mathlib/Topology/ContinuousFunction/Algebra.lean

feat: minimize requirements for inv/neg on C(X, Y) (#9758)

Modified ContinuousMap.coe_inv View on Github →

2023-05-08 21:09

Mathlib/Topology/ContinuousFunction/Algebra.lean

feat: port Topology.ContinuousFunction.Algebra (#3332)

Added ContinuousMap.coe_inv View on Github →