Theorem EuclideanSpace.ball_zero_eq

Modification history

2023-10-24 09:40
Mathlib/Analysis/InnerProductSpace/PiL2.lean
feat: volume of a complex ball (#6907) …
Added EuclideanSpace.ball_zero_eqView on Github →