Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-19 04:40 7d1ab388

View on Github →

feat(list/basic,...): minor modifications & additions based on Zulip conversations and requests

Estimated changes

Modified algebra/group.lean

Modified algebra/ring.lean

deleted def nonunits

Modified data/list/basic.lean

modified theorem list.append_inj_left'

modified theorem list.append_inj_left

modified theorem list.append_inj_right'

modified theorem list.append_inj_right

modified theorem list.append_left_cancel

added theorem list.append_left_inj

modified theorem list.append_right_cancel

added theorem list.append_right_inj

added theorem list.drop_suffix

added theorem list.prefix_append_left_inj

added theorem list.prefix_cons_inj

added theorem list.prefix_iff_eq_append

added theorem list.prefix_iff_eq_take

added theorem list.suffix_iff_eq_append

added theorem list.suffix_iff_eq_drop

added theorem list.take_prefix

Modified data/set/basic.lean

modified theorem set.image_preimage_eq

modified theorem set.preimage_image_eq

Modified logic/basic.lean

modified def decidable_of_iff'

modified def decidable_of_iff

added theorem exists_prop_of_false

added theorem exists_prop_of_true

added theorem forall_prop_of_false

added theorem forall_prop_of_true

modified theorem not_and_not_right

modified theorem not_and_of_not_or_not

modified theorem not_imp_of_and_not

added theorem not_nonempty_iff_imp_false

Modified ring_theory/ideals.lean

added def nonunits