Revision #1928 → #2480 · back to history
modifiedInner automorphism map Ψ35d66cf8bbeb
| Field | From #1928 | To #2480 |
|---|
| mathlib.module | Mathlib.Algebra.Group.Aut | Mathlib.Algebra.Group.End |
| note | Mathlib has `MulAut.conj` for the abstract group inner-automorphism map, but not the smooth Lie group inner automorphism Ψ_g : G → Aut(G). | Mathlib has `MulAut.conj : G →* MulAut G` (the abstract group inner-automorphism map) but not the smooth Lie group inner automorphism Ψ_g. |
addedAd_g is a Lie algebra automorphism5f3a5ec2d378
modifiedad_z is a derivation (Leibniz law)cac69131f0a5
| Field | From #1928 | To #2480 |
|---|
| anchor.snippet | the linear mapping | obeys the Leibniz' law |
| provenance | ai | ai-moderated |
modifiedad is differential of Ad at identity7ab9963a5d59
| Field | From #1928 | To #2480 |
|---|
| anchor.snippet | When | ad is the differential of Ad at the identity element of G |
| provenance | ai | ai-moderated |
addedKernel of Ad is centralizer of identity componentb9ddc00c33fc
addedFirst isomorphism theorem for Adcdc6bc54183d
modifiedImage of adjoint representation equals adjoint groupc423c0b94d13
| Field | From #1928 | To #2480 |
|---|
| anchor.snippet | Now, if | is the image of the adjoint representation of G |
| provenance | ai | ai-moderated |
modifiedRoot system of SL(2, R)3dc08d4a6930
| Field | From #1928 | To #2480 |
|---|
| mathlib.decl | LieAlgebra.sl2 | IsSl2Triple |
| note | `Mathlib.Algebra.Lie.Sl2` develops sl₂-triples, but the explicit A₁ root system computation for sl(2,ℝ) is not given. | `Mathlib.Algebra.Lie.Sl2` develops `IsSl2Triple` and sl₂-triple theory, but the explicit A₁ root system computation for sl(2,ℝ) is not given. |