Theorem InnerProductGeometry.mul_norm_eq_abs_sub_sq_norm

Modification history

2025-09-21 21:23
Mathlib/Geometry/Euclidean/Sphere/Power.lean
feat(Geometry/Euclidean/Sphere/Power): use side condition `p ∈ line[ℝ, a, b]` (#29344) …
Modified InnerProductGeometry.mul_norm_eq_abs_sub_sq_normView on Github →
2023-05-27 14:09
Mathlib/Geometry/Euclidean/Sphere/Power.lean
feat: port Geometry.Euclidean.Sphere.Power (#4418)
Added InnerProductGeometry.mul_norm_eq_abs_sub_sq_normView on Github →