Commit 2024-08-20 19:19 f904bf86
View on Github →chore: Better names for (⌊a⌋₊ : α) = ⌊a⌋
again (#16001)
Also remove the six months old deprecated names
chore: Better names for (⌊a⌋₊ : α) = ⌊a⌋
again (#16001)
Also remove the six months old deprecated names