Commit 2026-08-22 16:44 c38284bc

View on Github →

chore: deprecate Mathlib.Data.Finite.Vector (#43033) since #38743 merged it into Mathlib.Data.Fintype.Vector

Estimated changes

Modified Mathlib/Data/Finite/Vector.lean

Modified Mathlib/Data/Set/Finite/List.lean

modified theorem List.finite_length_eq