Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-31 07:44 dc1525fb

View on Github →

docs(data/sum/basic): Expand module docstring and cleanup (#11158) This moves data.sum to data.sum.basic, provides a proper docstring for it, cleans it up. There are no new declarations, just some file rearrangement, variable grouping, unindentation, and a protected attribute for sum.lex.inl/sum.lex.inr to avoid them clashing with sum.inl/sum.inr.

Estimated changes

modified theorem function.injective.sum_elim
deleted theorem sum.exists
deleted theorem sum.forall
modified def sum.get_left
modified def sum.get_right
modified theorem sum.inl_injective
modified theorem sum.inr_injective
modified def sum.is_left
modified def sum.is_right
added theorem sum.lex.mono
added theorem sum.lex.mono_left
added theorem sum.lex.mono_right
modified inductive sum.lex
modified theorem sum.lex_acc_inl
modified theorem sum.lex_acc_inr
modified theorem sum.lex_inl_inl
modified theorem sum.lex_inr_inl
modified theorem sum.lex_inr_inr
modified theorem sum.lex_wf
modified theorem sum.swap_left_inverse
modified theorem sum.swap_right_inverse
modified theorem sum.swap_swap
modified theorem sum.swap_swap_eq
modified theorem sum.update_elim_inl
modified theorem sum.update_elim_inr
modified theorem sum.update_inl_apply_inl
modified theorem sum.update_inl_apply_inr
modified theorem sum.update_inl_comp_inl
modified theorem sum.update_inl_comp_inr
modified theorem sum.update_inr_apply_inl
modified theorem sum.update_inr_apply_inr
modified theorem sum.update_inr_comp_inl
modified theorem sum.update_inr_comp_inr
added theorem sum.«exists»
added theorem sum.«forall»