Commit 2024-10-24 21:25 0b6c6c4d

View on Github →

feat: use aliases for CovariantClass α α (· * ·) (· ≤ ·) etc (#13154)

Estimated changes

modified theorem List.Sublist.prod_le_prod'
modified theorem List.exists_le_of_prod_le'
modified theorem List.exists_lt_of_prod_lt'
modified theorem List.one_le_prod_of_one_le
modified theorem List.pow_card_le_prod
modified theorem List.prod_le_pow_card
modified theorem List.prod_le_prod'
modified theorem List.prod_lt_prod'
modified theorem List.prod_lt_prod_of_ne_nil
modified theorem List.prod_min_le
modified theorem inf_div
modified theorem inf_mul
modified theorem inf_mul_sup
modified theorem mul_inf
modified theorem mul_sup
modified theorem sup_div
modified theorem sup_mul
modified theorem cmp_div_one'
modified theorem div_le_inv_mul_iff
modified theorem lt_iff_exists_mul
modified theorem one_le_two'
modified theorem one_le_two
modified theorem one_lt_two
modified theorem zero_le_four
modified theorem zero_le_three
modified theorem zero_le_two
modified theorem Antitone.const_mul'
modified theorem Antitone.mul'
modified theorem Antitone.mul_const'
modified theorem Antitone.mul_strictAnti'
modified theorem AntitoneOn.const_mul'
modified theorem AntitoneOn.mul'
modified theorem AntitoneOn.mul_const'
modified theorem AntitoneOn.mul_strictAnti'
modified theorem Left.mul_le_one
modified theorem Left.mul_lt_mul
modified theorem Left.mul_lt_one'
modified theorem Left.mul_lt_one
modified theorem Left.mul_lt_one_of_le_of_lt
modified theorem Left.mul_lt_one_of_lt_of_le
modified theorem Left.one_le_mul
modified theorem Left.one_lt_mul'
modified theorem Left.one_lt_mul
modified theorem Left.one_lt_mul_of_le_of_lt
modified theorem Left.one_lt_mul_of_lt_of_le
modified theorem Monotone.const_mul'
modified theorem Monotone.mul'
modified theorem Monotone.mul_const'
modified theorem Monotone.mul_strictMono'
modified theorem MonotoneOn.const_mul'
modified theorem MonotoneOn.mul'
modified theorem MonotoneOn.mul_const'
modified theorem MonotoneOn.mul_strictMono'
modified theorem Right.mul_le_one
modified theorem Right.mul_lt_mul
modified theorem Right.mul_lt_one'
modified theorem Right.mul_lt_one
modified theorem Right.one_le_mul
modified theorem Right.one_lt_mul'
modified theorem Right.one_lt_mul
modified theorem StrictAnti.mul'
modified theorem StrictAntiOn.mul'
modified theorem StrictMono.mul'
modified theorem StrictMonoOn.mul'
modified theorem cmp_mul_left'
modified theorem exists_square_le
modified theorem le_mul_iff_one_le_left'
modified theorem le_mul_iff_one_le_right'
modified theorem le_mul_of_le_mul_left
modified theorem le_mul_of_le_mul_right
modified theorem le_mul_of_le_of_one_le
modified theorem le_mul_of_one_le_left'
modified theorem le_mul_of_one_le_of_le
modified theorem le_mul_of_one_le_right'
modified theorem le_of_le_mul_of_le_one_left
modified theorem le_of_mul_le_mul_left'
modified theorem le_of_mul_le_mul_right'
modified theorem le_of_mul_le_of_one_le_left
modified theorem le_one_of_mul_le_left
modified theorem le_one_of_mul_le_right
modified theorem lt_mul_iff_one_lt_left'
modified theorem lt_mul_iff_one_lt_right'
modified theorem lt_mul_of_le_of_one_lt
modified theorem lt_mul_of_lt_mul_left
modified theorem lt_mul_of_lt_mul_right
modified theorem lt_mul_of_lt_of_one_le
modified theorem lt_mul_of_lt_of_one_lt'
modified theorem lt_mul_of_lt_of_one_lt
modified theorem lt_mul_of_one_le_of_lt
modified theorem lt_mul_of_one_lt_left'
modified theorem lt_mul_of_one_lt_of_le
modified theorem lt_mul_of_one_lt_of_lt'
modified theorem lt_mul_of_one_lt_of_lt
modified theorem lt_mul_of_one_lt_right'
modified theorem lt_of_lt_mul_of_le_one_left
modified theorem lt_of_mul_lt_mul_left'
modified theorem lt_of_mul_lt_mul_right'
modified theorem lt_of_mul_lt_of_one_le_left
modified theorem lt_one_of_mul_lt_left
modified theorem lt_one_of_mul_lt_right
modified theorem mulLECancellable_mul
modified theorem mul_eq_mul_iff_eq_and_eq
modified theorem mul_eq_one_iff_of_one_le
modified theorem mul_le_iff_le_one_left'
modified theorem mul_le_iff_le_one_right'
modified theorem mul_le_mul'
modified theorem mul_le_mul_iff_left
modified theorem mul_le_mul_iff_of_ge
modified theorem mul_le_mul_iff_right
modified theorem mul_le_mul_left'
modified theorem mul_le_mul_right'
modified theorem mul_le_mul_three
modified theorem mul_le_of_le_of_le_one
modified theorem mul_le_of_le_one_left'
modified theorem mul_le_of_le_one_of_le
modified theorem mul_le_of_le_one_right'
modified theorem mul_le_of_mul_le_left
modified theorem mul_le_of_mul_le_right
modified theorem mul_left_cancel''
modified theorem mul_lt_iff_lt_one_left'
modified theorem mul_lt_iff_lt_one_right'
modified theorem mul_lt_mul_iff_left
modified theorem mul_lt_mul_iff_right
modified theorem mul_lt_mul_left'
modified theorem mul_lt_mul_of_le_of_lt
modified theorem mul_lt_mul_of_lt_of_le
modified theorem mul_lt_mul_of_lt_of_lt
modified theorem mul_lt_mul_right'
modified theorem mul_lt_of_le_of_lt_one
modified theorem mul_lt_of_le_one_of_lt
modified theorem mul_lt_of_lt_of_le_one
modified theorem mul_lt_of_lt_of_lt_one'
modified theorem mul_lt_of_lt_of_lt_one
modified theorem mul_lt_of_lt_one_left'
modified theorem mul_lt_of_lt_one_of_le
modified theorem mul_lt_of_lt_one_of_lt'
modified theorem mul_lt_of_lt_one_of_lt
modified theorem mul_lt_of_lt_one_right'
modified theorem mul_lt_of_mul_lt_left
modified theorem mul_lt_of_mul_lt_right
modified theorem mul_right_cancel''
modified theorem one_le_of_le_mul_left
modified theorem one_le_of_le_mul_right
modified theorem one_lt_of_lt_mul_left
modified theorem one_lt_of_lt_mul_right
modified theorem exists_one_le_mul_of_le
modified theorem exists_one_lt_mul_of_lt'
modified theorem le_iff_exists_one_le_mul
modified theorem lt_iff_exists_one_lt_mul
modified theorem le_or_le_of_mul_le_mul
modified theorem le_or_lt_of_mul_le_mul
modified theorem lt_or_le_of_mul_le_mul
modified theorem lt_or_lt_of_mul_lt_mul
modified theorem max_le_mul_of_one_le
modified theorem min_le_mul_of_one_le_left
modified theorem min_le_mul_of_one_le_right
modified theorem mul_lt_mul_iff_of_le_of_le
modified theorem Left.pow_lt_one_iff'
modified theorem Left.pow_lt_one_iff
modified theorem Right.pow_lt_one_iff
modified theorem add_le_mul_two_add
modified theorem add_one_le_two_mul
modified theorem Nonneg.mk_add_mk
modified theorem Nonneg.nsmul_mk
modified theorem Even.tsub
modified theorem Tropical.add_pow
modified theorem Finset.fold_max_add
modified theorem Left.sign_neg
modified theorem Right.sign_neg
modified theorem QuadraticMap.PosDef.add
modified theorem QuadraticMap.PosDef.prod
modified theorem MeasureTheory.one_le_div_ae
modified theorem ciSup_mul_ciSup_le
modified theorem ciSup_mul_le
modified theorem le_ciInf_mul
modified theorem le_ciInf_mul_ciInf
modified theorem le_mul_ciInf
modified theorem mul_ciSup_le