Commit 2023-07-03 11:03 d450fcd7

View on Github →

fix: precedence of # (#5623)

Estimated changes

modified theorem Cardinal.mk_quaternion
modified theorem Cardinal.mk_univ_quaternion
modified theorem mk_complex
modified theorem mk_univ_complex
modified theorem Cardinal.mkRat
modified theorem Cardinal.mk_Icc_real
modified theorem Cardinal.mk_Ici_real
modified theorem Cardinal.mk_Ico_real
modified theorem Cardinal.mk_Iic_real
modified theorem Cardinal.mk_Iio_real
modified theorem Cardinal.mk_Ioc_real
modified theorem Cardinal.mk_Ioi_real
modified theorem Cardinal.mk_Ioo_real
modified theorem Cardinal.mk_real
modified theorem Cardinal.mk_univ_real
modified theorem WType.cardinal_mk_eq_sum
modified theorem WType.cardinal_mk_le_of_le
modified theorem Field.nonempty_iff
modified theorem Basis.le_span
modified theorem Basis.mk_eq_rank''
modified theorem Basis.mk_range_eq_rank
modified theorem mk_eq_mk_of_basis'
modified theorem rank_span_le
modified theorem rank_finsupp'
modified theorem rank_finsupp_self'
modified theorem rank_finsupp_self
modified theorem IsLocalization.card
modified theorem IsLocalization.card_le
modified theorem Cardinal.add_def
modified theorem Cardinal.aleph0_le_mk
modified theorem Cardinal.card_le_of
modified theorem Cardinal.card_le_of_finset
modified theorem Cardinal.denumerable_iff
modified theorem Cardinal.eq_one_iff_unique
modified theorem Cardinal.inductionOn
modified theorem Cardinal.infinite_iff
modified theorem Cardinal.le_def
modified theorem Cardinal.le_mk_diff_add_mk
modified theorem Cardinal.lift_mk_eq'
modified theorem Cardinal.lift_mk_fin
modified theorem Cardinal.lift_mk_le'
modified theorem Cardinal.mk'_def
modified theorem Cardinal.mk_Prop
modified theorem Cardinal.mk_arrow
modified theorem Cardinal.mk_bool
modified theorem Cardinal.mk_coe_finset
modified theorem Cardinal.mk_congr
modified theorem Cardinal.mk_denumerable
modified theorem Cardinal.mk_diff_add_mk
modified theorem Cardinal.mk_empty
modified theorem Cardinal.mk_emptyCollection
modified theorem Cardinal.mk_eq_aleph0
modified theorem Cardinal.mk_eq_nat_iff
modified theorem Cardinal.mk_eq_one
modified theorem Cardinal.mk_eq_two_iff'
modified theorem Cardinal.mk_eq_two_iff
modified theorem Cardinal.mk_eq_zero
modified theorem Cardinal.mk_eq_zero_iff
modified theorem Cardinal.mk_fin
modified theorem Cardinal.mk_fintype
modified theorem Cardinal.mk_iUnion_le
modified theorem Cardinal.mk_image_eq
modified theorem Cardinal.mk_image_le
modified theorem Cardinal.mk_int
modified theorem Cardinal.mk_le_aleph0
modified theorem Cardinal.mk_le_aleph0_iff
modified theorem Cardinal.mk_le_mk_of_subset
modified theorem Cardinal.mk_le_of_injective
modified theorem Cardinal.mk_list_eq_sum_pow
modified theorem Cardinal.mk_nat
modified theorem Cardinal.mk_ne_zero
modified theorem Cardinal.mk_ne_zero_iff
modified theorem Cardinal.mk_option
modified theorem Cardinal.mk_out
modified theorem Cardinal.mk_pNat
modified theorem Cardinal.mk_pempty
modified theorem Cardinal.mk_pi
modified theorem Cardinal.mk_plift_false
modified theorem Cardinal.mk_plift_true
modified theorem Cardinal.mk_powerset
modified theorem Cardinal.mk_prod
modified theorem Cardinal.mk_psum
modified theorem Cardinal.mk_punit
modified theorem Cardinal.mk_quot_le
modified theorem Cardinal.mk_quotient_le
modified theorem Cardinal.mk_range_eq
modified theorem Cardinal.mk_range_le
modified theorem Cardinal.mk_sUnion_le
modified theorem Cardinal.mk_sep
modified theorem Cardinal.mk_set
modified theorem Cardinal.mk_set_le
modified theorem Cardinal.mk_sigma
modified theorem Cardinal.mk_singleton
modified theorem Cardinal.mk_subtype_le
modified theorem Cardinal.mk_sum
modified theorem Cardinal.mk_sum_compl
modified theorem Cardinal.mk_toNat_eq_card
modified theorem Cardinal.mk_uLift
modified theorem Cardinal.mk_union_le
modified theorem Cardinal.mk_unit
modified theorem Cardinal.mk_univ
modified theorem Cardinal.mk_vector
modified theorem Cardinal.mul_def
modified theorem Cardinal.power_def
modified theorem Cardinal.prod_const'
modified theorem Cardinal.sum_const'
modified theorem Cardinal.sum_le_iSup
modified theorem Cardinal.three_le
modified theorem Cardinal.toNat_congr
modified theorem Cardinal.toPartENat_congr
modified theorem Cardinal.two_le_iff'
modified theorem Cardinal.two_le_iff
modified theorem Cardinal.derivFamily_lt_ord
modified theorem Cardinal.mk_bounded_subset
modified theorem Order.cof_le
modified theorem Ordinal.cof_eq
modified theorem Ordinal.cof_lsub_le
modified theorem Ordinal.cof_type_le
modified theorem Ordinal.iSup_lt
modified theorem Ordinal.infinite_pigeonhole
modified theorem Ordinal.le_cof_type
modified theorem Ordinal.lsub_lt_ord
modified theorem Ordinal.lt_cof_type
modified theorem Ordinal.nfpFamily_lt_ord
modified theorem Ordinal.sup_lt_ord
modified theorem Ordinal.sup_lt_ord_lift
modified theorem Cardinal.mk_set_nat
modified theorem Cardinal.add_mk_eq_max'
modified theorem Cardinal.add_mk_eq_max
modified theorem Cardinal.aleph0_mul_mk_eq
modified theorem Cardinal.mk_add_one_eq
modified theorem Cardinal.mk_cardinal
modified theorem Cardinal.mk_finsupp_nat
modified theorem Cardinal.mk_list_eq_aleph0
modified theorem Cardinal.mk_list_eq_mk
modified theorem Cardinal.mk_list_le_max
modified theorem Cardinal.mk_mul_aleph0_eq
modified theorem Cardinal.mul_mk_eq_max
modified theorem Cardinal.card_typein_lt
modified theorem Cardinal.mk_ord_out
modified theorem Cardinal.mk_ordinal_out
modified theorem Cardinal.ord_eq
modified theorem Cardinal.ord_eq_Inf
modified theorem Cardinal.ord_le_type
modified theorem Cardinal.univ_id
modified theorem Ordinal.card_type