Commit 2024-01-19 09:25 8fb1d5ae

View on Github →

chore: remove duplicates about List.append (#9376) Replace duplicates in Mathlib with theorems in Lean core.

List.append_left_cancel → List.append_cancel_left
List.append_right_cancel → List.append_cancel_right

Estimated changes

Modified Mathlib/Algebra/FreeMonoid/Basic.lean

Modified Mathlib/Computability/TuringMachine.lean

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.append_left_cancel

deleted theorem List.append_right_cancel

Modified Mathlib/Data/List/Infix.lean