Skip to content

[Merged by Bors] - chore: move Data/Real/GoldenRatio and RingTheory/Real/Irrational to NumberTheory/Real #6182

[Merged by Bors] - chore: move Data/Real/GoldenRatio and RingTheory/Real/Irrational to NumberTheory/Real

[Merged by Bors] - chore: move Data/Real/GoldenRatio and RingTheory/Real/Irrational to NumberTheory/Real #6182

Triggered via pull request October 16, 2025 08:27
Status Success
Total duration 42s
Artifacts

pre-commit.yml

on: pull_request
Fit to window
Zoom out
Zoom in