Commit 2023-10-24 09:40 a9da37b0
View on Github →feat: volume of a complex ball (#6907) We prove the formula for the area of a disc
theorem volume_ball (x : EuclideanSpace ℝ (Fin 2)) (r : ℝ) :
volume (Metric.ball x r) = NNReal.pi * (ENNReal.ofReal r) ^ 2
and deduce from this, the volume of complex balls
theorem volume_ball (a : ℂ) (r : ℝ) :
volume (Metric.ball a r) = NNReal.pi * (ENNReal.ofReal r) ^ 2