Theorem ne_neg_of_mem_sphere

Modification history

2025-10-17 16:01

Mathlib/Analysis/Normed/Module/Ball/Action.lean

chore(Algebra/Group/EvenFunction): don't import torsion-free modules (#30628) …

Modified ne_neg_of_mem_sphere View on Github →

2023-04-19 11:19

Mathlib/Analysis/NormedSpace/BallAction.lean

feat: port Analysis.NormedSpace.BallAction (#3513)

Added ne_neg_of_mem_sphere View on Github →