Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-09 07:26 7b1945e9

View on Github →

feat(logic/basic): dite_eq_ite (#6095) Simplify dite to ite when possible.

Estimated changes

Modified src/data/real/golden_ratio.lean

Modified src/group_theory/perm/sign.lean

Modified src/logic/basic.lean

added theorem dite_eq_ite