Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-29 04:24 ead85e61

View on Github →

chore(*/equiv): add simp to refl_apply and trans_apply where missing (#13760)

Estimated changes

Modified src/algebra/algebra/basic.lean

modified theorem alg_equiv.trans_apply

Modified src/algebra/hom/equiv.lean

Modified src/linear_algebra/affine_space/affine_equiv.lean

modified theorem affine_equiv.refl_apply

Modified src/order/hom/basic.lean

modified theorem order_iso.refl_apply

modified theorem order_iso.trans_apply