Revision #1359 → #1839 · back to history
modifiedGeneral linear group GL(2,R)23b7dd17b9bd
| Field | From #1359 | To #1839 |
|---|
| anchors | [{"section":"First examples","snippet":"The 2×2 real invertible matrices form a group under multiplication, called general linear group of degree 2"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {GL} (2,\\mathbb {R} )=\\left\\{A={\\begin{pmatrix}a&b\\\\c&d\\end{pmatrix}}:\\det A=ad-bc\\neq 0\\right\\}.}"}] | — |
modifiedRotation group SO(2)5f9145aaafff
| Field | From #1359 | To #1839 |
|---|
| anchors | [{"section":"First examples","snippet":"The rotation matrices form a subgroup"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {SO} (2,\\mathbb {R} )=\\left\\{{\\begin{pmatrix}\\cos \\varphi &-\\sin \\varphi \\\\\\sin \\varphi &\\cos \\varphi \\end{pmatrix}}:\\varphi \\in \\mathbb {R} \\ /\\ 2\\pi \\mathbb {Z} \\right\\}.}"}] | — |
| note | `Matrix.specialOrthogonalGroup n R` is defined, with a specialization `mem_specialOrthogonalGroup_fin_two_iff` for SO(2). | `Matrix.specialOrthogonalGroup n R` is defined, with a specialization `Matrix.mem_specialOrthogonalGroup_fin_two_iff` for SO(2). |
modifiedAffine group of one dimensionf5b84e22c644
| Field | From #1359 | To #1839 |
|---|
| anchors | [{"section":"First examples","snippet":"The affine group of one dimension is a two-dimensional matrix Lie group"},{"type":"math_alttext","value":"{\\displaystyle A=\\left({\\begin{array}{cc}a&b\\\\0&1\\end{array}}\\right),\\quad a>0,\\,b\\in \\mathbb {R} .}"}] | — |
modifiedExponential map (matrix case)099fc3616837
| Field | From #1359 | To #1839 |
|---|
| mathlib.module | Mathlib.Analysis.Normed.Algebra.MatrixExponential | Mathlib.Analysis.Normed.Algebra.Exponential |
| note | The matrix exponential is `NormedSpace.exp` applied to matrices, with dedicated lemmas like `Matrix.exp_add_of_commute`. | The matrix exponential is `NormedSpace.exp` applied to matrices, with dedicated lemmas like `Matrix.exp_add_of_commute` in `Mathlib.Analysis.Normed.Algebra.MatrixExponential`. |
addedUniversal cover of a connected Lie group is a Lie groupb20a0642e1e3
addedQuotient of a Lie group by a closed normal subgroup is a Lie groupaa2830029c83
addedLie bracket of GL(n,C) is the matrix commutator49e2db396b3a
addedSO(3) is not simply connected7d7552a7a8bd
addedIdentity component is an open normal subgroup with discrete quotientec6b7596db50
addedDiffeomorphism group acts transitively on a Lie groupee787055f931