[Merged by Bors] - feat: sync Data.Vector.Basic #2659
Closed
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
data.vector.basic
@9003f28797c0664a49e4179487267c494477d853
..f694c7dead66f5d4c80f446c796a5aad14707f0e
This has two changes:
Vector.replicate
: In Mathlib4 this definition is inData/Vector.lean
: docs4#Vector.replicatenth_repeat
tonth_replicate
: This has the nameget_replicate
in mathlib4, see docs4#Vector.get_replicateI don't know the background behind this diverge, but it seems that this diff might be marked as synced.