Mathlib Changelog
v4
Changelog
About
Github
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_sphere
View on Github →