Commit 2023-04-10 18:08 f7ed2abd

View on Github →

feat: port Init.IteSimp (#3368)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Finsupp/Antidiagonal.lean

Modified Mathlib/Data/List/Defs.lean

Created Mathlib/Init/IteSimp.lean

added theorem if_false_left_eq_and

added theorem if_false_right_eq_and

added theorem if_true_left_eq_or

added theorem if_true_right_eq_or