Theorem InnerProductGeometry.norm_withLpEquiv_crossProduct

Modification history

2025-12-29 03:44
Mathlib/Geometry/Euclidean/Angle/Unoriented/CrossProduct.lean
chore: remove May 2025 deprecated declarations (#33014) …
Deleted InnerProductGeometry.norm_withLpEquiv_crossProductView on Github →
2025-02-05 22:11
Mathlib/Geometry/Euclidean/Angle/Unoriented/CrossProduct.lean
feat: add theorem about the norm of cross products (#20920) …
Added InnerProductGeometry.norm_withLpEquiv_crossProductView on Github →