Commit 2024-12-20 12:30 0719ca8f

View on Github →

chore: rename List.Vector.get_eq_get (#20087)

Estimated changes

Modified Mathlib/Computability/Primrec.lean

Modified Mathlib/Data/Vector/Basic.lean

deleted theorem List.Vector.get_eq_get

added theorem List.Vector.get_eq_get_toList

Modified Mathlib/Data/Vector/Mem.lean