Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-14 07:40 f727e126

View on Github →

chore(logic/basic): tidy ite section and misplaced lemmas (#10761) Moves a few lemmas down and use variables.

Estimated changes

modified theorem apply_dite2
modified theorem apply_dite
modified theorem apply_ite2
modified theorem apply_ite
modified theorem dite_apply
modified theorem dite_eq_ite
modified theorem dite_not
modified theorem ite_and
modified theorem ite_apply
modified theorem ite_eq_iff
modified theorem ite_eq_left_iff
modified theorem ite_eq_or_eq
modified theorem ite_eq_right_iff
modified theorem ite_not