Revision #3277 → #3812 · back to history
modifiedSchläfli symbol and symmetry group0985b4a0293f
| Field | From #3277 | To #3812 |
|---|
| note | The dihedral group D₅ exists in Mathlib as `DihedralGroup 5`, but it is not connected to a pentagram symmetry group; Schläfli symbols are absent. | The dihedral group D₅ exists in Mathlib as `DihedralGroup 5` (verified via decl_exists), but it is not connected to a pentagram symmetry group; Schläfli symbols are absent. |
modifiedGolden ratio in pentagram edgesa3588bf0db3e
| Field | From #3277 | To #3812 |
|---|
| note | `Real.goldenRatio` (φ) is defined in Mathlib, but its geometric appearance in pentagram edge sections is not formalized. | `Real.goldenRatio` (φ) is defined in Mathlib (verified via decl_exists), but its geometric appearance in pentagram edge sections is not formalized. |
addedRegular pentagon26c06b2feab1
addedStar polygon06406fa7acc1
addedGolden gnomonb686be50a96b
addedGolden triangle7461206f2dd1