Commit 2022-10-23 22:23 d4ca349a

View on Github →

chore: port Init.Propext (#471) Porting anything trivial to port which contains lemmas mentioned by mathlib3's norm_num or ring.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Init/Propext.lean

added theorem Iff.to_eq

added theorem eq_false_intro

added theorem eq_true_intro

added theorem iff_eq_eq

added theorem imp_congr_ctx_eq

added theorem imp_congr_eq