Theorem ContinuousMap.isUnit_iff_forall_ne_zero

Modification history

2024-04-19 02:04

Mathlib/Topology/ContinuousFunction/Units.lean

feat(Analysis/SpecificLimits/Normed): generalize to division rings (#12164)

Modified ContinuousMap.isUnit_iff_forall_ne_zero View on Github →

2023-06-08 04:21

Mathlib/Topology/ContinuousFunction/Units.lean

feat: port Topology.ContinuousFunction.Units (#4818)

Added ContinuousMap.isUnit_iff_forall_ne_zero View on Github →