Revision #1137 → #1764 · back to history
modifiedFace diagonal of the cube9b97be2a2912
| Field | From #1137 | To #1764 |
|---|
| anchors | [{"section":"Measurement","snippet":"the face diagonal of the cube is the diagonal of a square"},{"type":"math_alttext","value":"{\\displaystyle A=6a^{2}.}"},{"type":"math_alttext","value":"{\\displaystyle V=a^{3}.}"}] | — |
modifiedSpace diagonal of the cube1d936047dc74
| Field | From #1137 | To #1764 |
|---|
| anchors | [{"section":"Measurement","snippet":"the space diagonal of the cube is a line connecting two vertices that are not in the same face"},{"type":"math_alttext","value":"{\\displaystyle A=6a^{2}.}"},{"type":"math_alttext","value":"{\\displaystyle V=a^{3}.}"}] | — |
modifiedSurface area of the cubeadd731b981b0
| Field | From #1137 | To #1764 |
|---|
| anchors | [{"section":"Measurement","snippet":"is six times the area of a square"},{"type":"math_alttext","value":"{\\displaystyle A=6a^{2}.}"},{"type":"math_alttext","value":"{\\displaystyle V=a^{3}.}"}] | — |
modifiedVolume of the cubeaec89e5821da
| Field | From #1137 | To #1764 |
|---|
| anchors | [{"section":"Measurement","snippet":"the formula for the volume of a cube is the third power of its side length"},{"type":"math_alttext","value":"{\\displaystyle A=6a^{2}.}"},{"type":"math_alttext","value":"{\\displaystyle V=a^{3}.}"}] | — |
modifiedInsphere, midsphere, and circumsphereb2b790713931
| Field | From #1137 | To #1764 |
|---|
| anchors | [{"section":"Measurement","snippet":"is a sphere tangent to the faces of a cube at their centroids"},{"type":"math_alttext","value":"{\\displaystyle r_{i}={\\frac {1}{2}}a=0.5a,\\qquad r_{m}={\\frac {\\sqrt {2}}{2}}a\\approx 0.707a,\\qquad r_{c}={\\frac {\\sqrt {3}}{2}}a\\approx 0.866a.}"}] | — |
modifiedCartesian coordinates of cube vertices9777c9f1aadb
| Field | From #1137 | To #1764 |
|---|
| anchors | [{"section":"Constructions","snippet":"the Cartesian coordinates of the vertices are"},{"type":"math_alttext","value":"{\\displaystyle \\max\\{|x-x_{0}|,|y-y_{0}|,|z-z_{0}|\\}=a.}"}] | — |
modifiedInterior of the cubeff132bc135d4
| Field | From #1137 | To #1764 |
|---|
| anchors | [{"section":"Constructions","snippet":"Its interior consists of all points"},{"type":"math_alttext","value":"{\\displaystyle \\max\\{|x-x_{0}|,|y-y_{0}|,|z-z_{0}|\\}=a.}"}] | — |
modifiedSurface of a cube as a locus1672a90920b5
| Field | From #1137 | To #1764 |
|---|
| anchors | [{"section":"Constructions","snippet":"A cube's surface with center"},{"type":"math_alttext","value":"{\\displaystyle \\max\\{|x-x_{0}|,|y-y_{0}|,|z-z_{0}|\\}=a.}"}] | — |
modifiedCubical graph is not complete bipartited4fccf0360d7
| Field | From #1137 | To #1764 |
|---|
| mathlib.module | Mathlib.Combinatorics.SimpleGraph.Bipartite | Mathlib.Combinatorics.SimpleGraph.Basic |
| note | `completeBipartiteGraph` is defined, but the statement that the cubical graph is not complete bipartite is not. | `completeBipartiteGraph` is defined in `SimpleGraph.Basic`, but the statement that the cubical graph is not complete bipartite is not. |
modifiedConfiguration matrix of the cube05e8b7a095e5
| Field | From #1137 | To #1764 |
|---|
| anchors | [{"section":"As a configuration matrix","snippet":"The cube can be represented as a configuration matrix"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{bmatrix}{\\begin{matrix}8&3&3\\\\2&12&2\\\\4&4&6\\end{matrix}}\\end{bmatrix}}}"}] | — |
modifiedRegular icosahedron from golden rectanglese1170d30fb4c
| Field | From #1137 | To #1764 |
|---|
| note | Although `goldenRatio` is in Mathlib, the icosahedron construction from golden rectangles is not. | The icosahedron construction from golden rectangles is not formalized. |
addedCartesian product of graphsecdc4138db54
addedCartesian product of three line segments7467ea8b6845
addedPolar reciprocation (dual polyhedron)486ebc4bf3cc
addedDual polyhedra share the same symmetry group21c10345c953