mathlib
3e2f2145 - feat(logic/basic): Generalize `congr_fun_heq` (#13867)

Commit

3 years ago

feat(logic/basic): Generalize `congr_fun_heq` (#13867) The lemma holds for arbitrary heterogeneous equalities, not only that given by casts.

Author

vihdzp

Parents