Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-29 17:31 ee8d588d

View on Github →

refactor(logic/hydra): use is_irrefl (#15039) is_irrefl seems to be the more commonly used spelling

Estimated changes

modified theorem acc.cut_expand
modified theorem relation.acc_of_singleton
modified theorem relation.cut_expand_iff