Commit 2025-08-24 19:45 6100c331
View on Github →chore(Data/Real/GoldenRatio): namespace, fix names (#28815)
The defs are called goldenRatio
/goldenConj
but were confusingly referred to as gold
/goldConj
in all lemma names.
chore(Data/Real/GoldenRatio): namespace, fix names (#28815)
The defs are called goldenRatio
/goldenConj
but were confusingly referred to as gold
/goldConj
in all lemma names.