Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-11 13:58 c2cc9a99

View on Github →

refactor(*): change priority of \simeq (#1210)

  • change priority of \simeq Also change priority of similar notations Remove many unnecessary parentheses
  • lower precedence on order_embedding and similar also add parentheses in 1 place where they were needed
  • spacing
  • add parenthesis

Estimated changes

modified def equiv.empty_prod
modified def equiv.empty_sum
modified def equiv.pempty_prod
modified def equiv.pempty_sum
modified def equiv.prod_assoc
modified def equiv.prod_comm
modified def equiv.prod_congr
modified def equiv.prod_empty
modified def equiv.prod_pempty
modified def equiv.prod_punit
modified def equiv.psum_equiv_sum
modified def equiv.punit_prod
modified theorem equiv.refl_trans
modified def equiv.sum_assoc
modified def equiv.sum_comm
modified def equiv.sum_congr
modified def equiv.sum_empty
modified def equiv.sum_pempty
modified theorem equiv.symm_symm
modified theorem equiv.symm_symm_apply
modified theorem equiv.trans_refl
modified def denumerable.pair
modified def fin_prod_fin_equiv
modified def sum_fin_sum_equiv
modified def initial_seg.lt_or_eq
modified def homeomorph.prod_assoc
modified def homeomorph.prod_comm
modified def homeomorph.prod_congr