Revision #3363 → #3907 · back to history
modifiedNorm scales by absolute value of real scalar3252901f8f91
| Field | From #3363 | To #3907 |
|---|
| mathlib.decl | Quaternion.instNormedAlgebra | Quaternion.instNormedAlgebraReal |
| note | The `NormedAlgebra ℝ ℍ` instance (and `Quaternion.norm_coe`) makes scalar multiplication norm-multiplicative: `‖r • q‖ = |r| * ‖q‖`. | The `NormedAlgebra ℝ ℍ` instance (`Quaternion.instNormedAlgebraReal`) makes scalar multiplication norm-multiplicative: `‖r • q‖ = |r| * ‖q‖`. |
modifiedNorm is multiplicative85d89787da50
| Field | From #3363 | To #3907 |
|---|
| mathlib.decl | Quaternion.instNormedDivisionRing | Quaternion.instNormedDivisionRingReal |
| note | The `NormedDivisionRing ℍ` instance bundles `norm_mul a b = ‖a‖ * ‖b‖`; `normSq` is also a `MonoidWithZeroHom`. | The `NormedDivisionRing ℍ` instance (`Quaternion.instNormedDivisionRingReal`) bundles `norm_mul a b = ‖a‖ * ‖b‖`; `normSq` is also a `MonoidWithZeroHom`. |
modifiedDistance between quaternions0d550a505d7e
| Field | From #3363 | To #3907 |
|---|
| mathlib.decl | Quaternion.instNormedAddCommGroup | Quaternion.instNormedAddCommGroupReal |
| note | Distance `dist a b = ‖a - b‖` follows from the `NormedAddCommGroup ℍ` instance. | Distance `dist a b = ‖a - b‖` follows from the `NormedAddCommGroup ℍ` instance (`Quaternion.instNormedAddCommGroupReal`). |
modifiedQuaternions form a metric spaceb1c1ab86322d
| Field | From #3363 | To #3907 |
|---|
| mathlib.decl | Quaternion.instNormedAddCommGroup | Quaternion.instNormedAddCommGroupReal |
modifiedUnit quaternion and versorfa791764d0f6
| Field | From #3363 | To #3907 |
|---|
| mathlib.decl | Quaternion.instNormOneClass | Quaternion.instNormOneClassReal |
modifiedArtin–Wedderburn theorem (Wedderburn's part)acb30bff2240
| Field | From #3363 | To #3907 |
|---|
| mathlib.decl | IsSemisimpleRing.isSemisimpleRing_iff_pi_matrix_divisionRing | isSemisimpleRing_iff_pi_matrix_divisionRing |
| note | `isSemisimpleRing_iff_pi_matrix_divisionRing` (and `exists_ringEquiv_matrix_divisionRing` for simple Artinian rings) is the Artin–Wedderburn structure theorem. | `isSemisimpleRing_iff_pi_matrix_divisionRing` (the existence part of Artin–Wedderburn) characterizes semisimple rings as finite products of matrix rings over division rings. |
addedOctonionsbacb283423b4
addedBiquaternionsac3d320baa9f
addedReal numbers embed in the quaternionsa0dd5a8672ca
addedNonzero quaternions have multiplicative inverses26a7b9f2d57a
addedQuaternions form a normed algebra over ℝd0ef0aa9116b