Theorem preimage_mul_ball

Modification history

2023-12-08 10:23

Mathlib/Analysis/Normed/Group/Basic.lean

chore: Replace `(· op ·) a` by `(a op ·)` (#8843) …

Modified preimage_mul_ball View on Github →

2023-03-09 06:58

Mathlib/Analysis/Normed/Group/Basic.lean

feat: port Analysis.Normed.Group.Basic (#2736)

Added preimage_mul_ball View on Github →