WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Euclidean vector

Revision #2448 → #2566 · back to history

modifiedLength of cross product is parallelogram area4496441d3037
FieldFrom #2448To #2566
mathlib.declnorm_crossProductInnerProductGeometry.norm_ofLp_crossProduct
provenanceaiai-moderated
modifiedTriple product multilinear and antisymmetric1c6a25b2470d
FieldFrom #2448To #2566
mathlib.declMatrix.det_row_alternatingMatrix.detRowAlternating
provenanceaiai-moderated