Commit 2022-08-22 17:24 d2111506
View on Github →chore: uncomment cons_injective and cons_inj in Data/List/Basic.lean (#372) Uncomment two theorems that were added in commented form in #22. You may compare to the mathlib3 versions here: https://github.com/leanprover-community/mathlib/blob/aaf7dc2c34831dbd92a21b9e37c1f63017d35f45/src/data/list/basic.lean#L50-L54