Theorem Real.inv_sqrt_two_sub_one

Modification history

2025-10-03 10:42
Mathlib/Data/Real/Sqrt.lean
feat(Probability): Fernique's theorem for distributions that are invariant by rotation (#28343) …
Added Real.inv_sqrt_two_sub_oneView on Github →