Commit 2022-10-08 09:24 089576b8

View on Github →

feat: minimal port of Fintype (Fin n) (#433)

depends on: #429

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Fin/Basic.lean

Modified Mathlib/Data/Fintype/Basic.lean

Modified Mathlib/Data/List/Basic.lean

added def List.attach

added theorem List.attach_map_val

added theorem List.map_pmap

added theorem List.mem_attach

added theorem List.mem_pmap

added def List.pmap

added theorem List.pmap_congr

added theorem List.pmap_eq_map

added theorem List.pmap_eq_map_attach

added theorem List.pmap_map

Created Mathlib/Data/List/Chain.lean

added theorem List.Chain.imp'

added theorem List.Chain.imp

added theorem List.chain_cons

added theorem List.chain_iff_pairwise

Created Mathlib/Data/List/Nodup.lean

added theorem List.Nodup.map_on

added theorem List.Nodup.of_map

added theorem List.Nodup.pmap

added theorem List.nodup_attach

Modified Mathlib/Data/List/Pairwise.lean

added theorem List.Pairwise.and_mem

added theorem List.Pairwise.iff_of_mem

added theorem List.Pairwise.imp

added theorem List.Pairwise.imp_of_mem

added theorem List.Pairwise.map

added theorem List.Pairwise.of_map

added theorem List.pairwise_map

added theorem List.pairwise_singleton

added theorem List.rel_of_pairwise_cons

Modified Mathlib/Data/List/Perm.lean

Created Mathlib/Data/List/Range.lean

added theorem List.chain_lt_range'

added theorem List.chain_succ_range'

added def List.finRange

added theorem List.fin_range_zero

added theorem List.mem_fin_range

added theorem List.mem_range'

added theorem List.mem_range

added theorem List.nodup_fin_range

added theorem List.nodup_range'

added theorem List.nodup_range

added theorem List.pairwise_lt_range'

added theorem List.rangeAux_range'

added theorem List.range_eq_range'

Modified Mathlib/Data/Multiset/Basic.lean

deleted def Mem

added def Multiset.Mem

Modified Mathlib/Logic/Basic.lean

added theorem Ball.imp_left

added theorem Ball.imp_right

added theorem forall_swap