Commit 2024-05-27 07:37 a5f75273

View on Github →

chore: Do not import algebra in Data.Vector (#13242) ... and rename Data.Vector to Data.Vector.Defs.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Trails.lean

Modified Mathlib/Computability/TuringMachine.lean

Modified Mathlib/Data/Finset/NAry.lean

Modified Mathlib/Data/Finset/NatAntidiagonal.lean

Modified Mathlib/Data/Finset/Prod.lean

Modified Mathlib/Data/Nat/Interval.lean

Modified Mathlib/Data/Sym/Basic.lean

Modified Mathlib/Data/Sym/Card.lean

Modified Mathlib/Data/Sym/Sym2.lean

Modified Mathlib/Data/Vector/Basic.lean

modified theorem Vector.get_append_cons_zero

modified theorem Vector.get_tail

Renamed Mathlib/Data/Vector.lean to Mathlib/Data/Vector/Defs.lean

Modified Mathlib/Order/Category/NonemptyFinLinOrd.lean

Modified Mathlib/RingTheory/Nilpotent/Defs.lean

Modified Mathlib/SetTheory/Game/PGame.lean

Modified test/NthRewrite.lean

Modified test/cc.lean