Theorem ne_neg_of_mem_unit_sphere

Modification history

2023-04-19 11:19
Mathlib/Analysis/NormedSpace/BallAction.lean
feat: port Analysis.NormedSpace.BallAction (#3513)
Added ne_neg_of_mem_unit_sphereView on Github →