Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-07-23 19:02 1b6322ff

View on Github →

chore(*): rfl-lemmas on same line

Estimated changes

modified theorem filter.mem_join_sets
modified theorem filter.mem_principal_sets
modified theorem filter.principal_empty
modified theorem filter.principal_univ
modified theorem set.fmap_eq_image
modified theorem set.set_of_mem_eq
modified theorem bool.bnot_false
modified theorem bool.bnot_true
modified theorem bool.cond_ff
modified theorem bool.cond_tt
modified theorem list.count_nil
modified theorem list.head_cons
modified theorem list.index_of_cons
modified theorem list.index_of_nil
modified theorem list.inth_succ
modified theorem list.inth_zero
modified theorem list.ith_zero
modified theorem list.last_singleton
modified theorem list.tail_cons
modified theorem list.tail_nil
modified theorem stream.all_def
modified theorem stream.any_def
modified theorem stream.approx_succ
modified theorem stream.approx_zero
modified theorem stream.composition
modified theorem stream.cons_append_stream
modified theorem stream.corec_def
modified theorem stream.drop_succ
modified theorem stream.even_tail
modified theorem stream.head_cons
modified theorem stream.head_even
modified theorem stream.head_iterate
modified theorem stream.head_map
modified theorem stream.head_zip
modified theorem stream.homomorphism
modified theorem stream.identity
modified theorem stream.inits_tail
modified theorem stream.interchange
modified theorem stream.map_const
modified theorem stream.map_eq_apply
modified theorem stream.map_id
modified theorem stream.map_map
modified theorem stream.map_tail
modified theorem stream.nil_append_stream
modified theorem stream.nth_const
modified theorem stream.nth_drop
modified theorem stream.nth_map
modified theorem stream.nth_nats
modified theorem stream.nth_succ
modified theorem stream.nth_zero_cons
modified theorem stream.nth_zero_iterate
modified theorem stream.nth_zip
modified theorem stream.odd_eq
modified theorem stream.tail_cons
modified theorem stream.tail_eq_drop
modified theorem stream.tail_zip
modified theorem stream.tails_eq_iterate