Revision #1060 → #1758 · back to history
11557c2ca201| Field | From #1060 | To #1758 |
|---|---|---|
| mathlib.decl | Basis | Module.Basis |
| note | A general (non-orthonormal) Basis provides oblique coordinates, but oblique systems are not separately named. | A general (non-orthonormal) Module.Basis provides oblique coordinates, but oblique systems are not separately named. |
73e800046545dced95c49030| Field | From #1060 | To #1758 |
|---|---|---|
| note | Orientation.rotation is rotation by an oriented angle in an oriented 2D inner product space, matching the cos/sin formula (cf. Complex.toMatrix_rotation). | Orientation.rotation is rotation by an oriented angle in an oriented 2D inner product space, matching the cos/sin formula. |
c112ac11f1b5| Field | From #1060 | To #1758 |
|---|---|---|
| mathlib.decl | reflection | Submodule.reflection |
| note | Reflection in a subspace specializes to axis reflections, but the coordinate formula (x,y)↦(-x,y) is not a stated lemma. | Submodule.reflection in a hyperplane specializes to axis reflections, but the coordinate formula (x,y)↦(-x,y) is not a stated lemma. |
2cad101a5604b6d6fb5f73cd| Field | From #1060 | To #1758 |
|---|---|---|
| anchors | [{"section":"General matrix form of the transformations","snippet":"All affine transformations of the plane can be described in a uniform way by using matrices."},{"type":"math_alttext","value":"{\\displaystyle {\\begin{pmatrix}x'\\\\y'\\end{pmatrix}}=A{\\begin{pmatrix}x\\\\y\\end{pmatrix}}+b,}"},{"type":"math_alttext","value":"{\\displaystyle A={\\begin{pmatrix}A_{1,1}&A_{1,2}\\\\A_{2,1}&A_{2,2}\\end{pmatrix}}}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}x'&=xA_{1,1}+yA_{1,1}+b_{1}\\\\y'&=xA_{2,1}+yA_{2,2}+b_{2}.\\end{aligned}}}"}] | [{"section":"General matrix form of the transformations","snippet":"All affine transformations of the plane can be described in a uniform way by using matrices."},{"type":"math_alttext","value":"{\\displaystyle {\\begin{pmatrix}x'\\\\y'\\end{pmatrix}}=A{\\begin{pmatrix}x\\\\y\\end{pmatrix}}+b,}"},{"type":"math_alttext","value":"{\\displaystyle A={\\begin{pmatrix}A_{1,1}&A_{1,2}\\\\A_{2,1}&A_{2,2}\\end{pmatrix}}}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}x'&=xA_{1,1}+yA_{1,1}+b_{1}\\\\y'&=xA_{2,1}+yA_{2,2}+b_{2}.\\end{aligned}}}"}] |
1b995507cb78| Field | From #1060 | To #1758 |
|---|---|---|
| note | SO(n) is formalized as specialOrthogonalGroup (with a 2×2 characterization), but the geometric iff for rotations about a point is not stated. | SO(n) is formalized as specialOrthogonalGroup, but the geometric iff for rotations about a point is not stated. |
191908516801| Field | From #1060 | To #1758 |
|---|---|---|
| anchors | [{"section":"General matrix form of the transformations","snippet":"transformations can be composed by simply multiplying the associated transformation matrices"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{pmatrix}x'\\\\y'\\\\1\\end{pmatrix}}=A'{\\begin{pmatrix}x\\\\y\\\\1\\end{pmatrix}},}"},{"type":"math_alttext","value":"{\\displaystyle A'={\\begin{pmatrix}A_{1,1}&A_{1,2}&b_{1}\\\\A_{2,1}&A_{2,2}&b_{2}\\\\0&0&1\\end{pmatrix}}.}"}] | [{"section":"General matrix form of the transformations","snippet":"transformations can be composed by simply multiplying the associated transformation matrices"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{pmatrix}x'\\\\y'\\\\1\\end{pmatrix}}=A'{\\begin{pmatrix}x\\\\y\\\\1\\end{pmatrix}},}"},{"type":"math_alttext","value":"{\\displaystyle A'={\\begin{pmatrix}A_{1,1}&A_{1,2}&b_{1}\\\\A_{2,1}&A_{2,2}&b_{2}\\\\0&0&1\\end{pmatrix}}.}"}] |
5dba9bcbe4d7| Field | From #1060 | To #1758 |
|---|---|---|
| anchors | [{"section":"Affine transformation","snippet":"Affine transformations of the Euclidean plane are transformations that map lines to lines"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{pmatrix}A_{1,1}&A_{2,1}&b_{1}\\\\A_{1,2}&A_{2,2}&b_{2}\\\\0&0&1\\end{pmatrix}}{\\begin{pmatrix}x\\\\y\\\\1\\end{pmatrix}}={\\begin{pmatrix}x'\\\\y'\\\\1\\end{pmatrix}}.}"}] | [{"section":"Affine transformation","snippet":"Affine transformations of the Euclidean plane are transformations that map lines to lines"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{pmatrix}A_{1,1}&A_{2,1}&b_{1}\\\\A_{1,2}&A_{2,2}&b_{2}\\\\0&0&1\\end{pmatrix}}{\\begin{pmatrix}x\\\\y\\\\1\\end{pmatrix}}={\\begin{pmatrix}x'\\\\y'\\\\1\\end{pmatrix}}.}"}] |
d36480292bdb| Field | From #1060 | To #1758 |
|---|---|---|
| mathlib.decl | positiveOrientation | Module.Oriented.positiveOrientation |
| note | positiveOrientation is the standard/positive orientation determined by the standard basis. | Module.Oriented.positiveOrientation is the standard/positive orientation determined by the standard basis. |
dd34fe418f62| Field | From #1060 | To #1758 |
|---|---|---|
| note | Complex.equivRealProd is the equivalence ℂ ≃ ℝ × ℝ identifying z = x + iy with (x, y) (with linear/CLM versions equivRealProdLm/equivRealProdCLM). | Complex.equivRealProd is the equivalence ℂ ≃ ℝ × ℝ identifying z = x + iy with (x, y). |
0ae5b95cf780