Commit 2023-11-09 04:02 a084bd51

View on Github →

style(SetTheory): remove useless parentheses (#8279) These were caused by a bad notation precedence in mathlib3, where the local version of ^ was given precedence 0. We're not using the local notation at all in Mathlib4 (partly because it was broken, which this PR fixes).

Estimated changes

modified theorem Cardinal.cantor'
modified theorem Cardinal.cantor
modified theorem Cardinal.le_powerlt
modified theorem Cardinal.lift_power
modified theorem Cardinal.lift_two_power
modified theorem Cardinal.mk_powerset
modified theorem Cardinal.mk_set
modified theorem Cardinal.mul_power
modified theorem Cardinal.natCast_pow
modified theorem Cardinal.one_power
modified theorem Cardinal.pow_cast_right
modified theorem Cardinal.power_add
modified theorem Cardinal.power_bit0
modified theorem Cardinal.power_bit1
modified theorem Cardinal.power_lt_aleph0
modified theorem Cardinal.power_mul
modified theorem Cardinal.power_ne_zero
modified theorem Cardinal.power_one
modified theorem Cardinal.power_pos
modified theorem Cardinal.power_zero
modified theorem Cardinal.powerlt_le
modified theorem Cardinal.powerlt_succ
modified theorem Cardinal.prod_const'
modified theorem Cardinal.self_le_power
modified theorem Cardinal.zero_power
modified theorem Cardinal.zero_power_le
modified theorem Ordinal.div_opow_log_lt
modified theorem Ordinal.div_opow_log_pos
modified theorem Ordinal.left_le_opow
modified theorem Ordinal.log_def
modified theorem Ordinal.log_mono_right
modified theorem Ordinal.log_nonempty
modified theorem Ordinal.log_opow
modified theorem Ordinal.lt_opow_iff_log_lt
modified theorem Ordinal.nat_cast_opow
modified theorem Ordinal.one_opow
modified theorem Ordinal.opow_add
modified theorem Ordinal.opow_dvd_opow
modified theorem Ordinal.opow_dvd_opow_iff
modified theorem Ordinal.opow_isLimit
modified theorem Ordinal.opow_isLimit_left
modified theorem Ordinal.opow_isNormal
modified theorem Ordinal.opow_le_iff_le_log
modified theorem Ordinal.opow_le_opow_left
modified theorem Ordinal.opow_le_opow_right
modified theorem Ordinal.opow_log_le_self
modified theorem Ordinal.opow_mul
modified theorem Ordinal.opow_mul_add_pos
modified theorem Ordinal.opow_ne_zero
modified theorem Ordinal.opow_one
modified theorem Ordinal.opow_one_add
modified theorem Ordinal.opow_pos
modified theorem Ordinal.opow_right_inj
modified theorem Ordinal.opow_succ
modified theorem Ordinal.opow_zero
modified theorem Ordinal.right_le_opow
modified theorem Ordinal.sup_opow_nat
modified theorem Ordinal.zero_opow'
modified theorem Ordinal.zero_opow