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

Diff — Cartesian coordinate system

Revision #2229 → #2904 · back to history

addedOrthogonal basis (axis directions)7cc2ae9377e0
addedUnit circle22e933b62c00
modifiedEuclidean transformations have orthogonal matrix2eed0558efe1
FieldFrom #2229To #2904
mathlib.declOrthonormalBasis.toMatrix_orthonormalBasis_mem_orthogonalMatrix.orthogonalGroup
mathlib.moduleMathlib.Analysis.InnerProductSpace.PiL2Mathlib.LinearAlgebra.UnitaryGroup
noteChange-of-orthonormal-basis matrices lie in the orthogonal group, but the iff characterization of plane Euclidean transformations is not stated.The orthogonal group Matrix.orthogonalGroup captures the matrices whose columns are orthonormal; Euclidean transformations correspond to affine maps whose linear part lies in this group, but the iff characterization is not stated.
provenanceaiai-moderated