Commit 2021-08-18 12:36 c0c69249

View on Github →

Merge branch 'master' of github.com:leanprover-community/mathlib4

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Int/Basic.lean

modified theorem Int.eq_x_or_neg

added theorem Int.eq_zero_ofNatAbs_eq_zero

deleted theorem Int.eq_zero_of_nat_abs_eq_zero

modified def Int.gcd

added theorem Int.mul_negSucc_ofNat_negSucc_ofNat

deleted theorem Int.mul_neg_succ_of_nat_neg_succ_of_nat

added theorem Int.natAbs_eq

added theorem Int.natAbs_mul_self

added theorem Int.natAbs_neg

added theorem Int.natAbs_ofNat

added theorem Int.natAbs_one

added theorem Int.natAbs_pos_of_ne_zero

added theorem Int.natAbs_zero

deleted def Int.nat_abs

deleted theorem Int.nat_abs_eq

deleted theorem Int.nat_abs_mul_self

deleted theorem Int.nat_abs_neg

deleted theorem Int.nat_abs_of_nat

deleted theorem Int.nat_abs_one

deleted theorem Int.nat_abs_pos_of_ne_zero

deleted theorem Int.nat_abs_zero

deleted def Int.nat_mod

added theorem Int.negOfNat_add

added theorem Int.negOfNat_eq_subNatNat_zero

added theorem Int.negOfNat_mul_negSucc_ofNat

added theorem Int.negOfNat_mul_ofNat

added theorem Int.negSucc_ofNat_add_negSucc_ofNat

added theorem Int.negSucc_ofNat_add_ofNat

added theorem Int.negSucc_ofNat_coe'

added theorem Int.negSucc_ofNat_coe

added theorem Int.negSucc_ofNat_eq

added theorem Int.negSucc_ofNat_inj_iff

added theorem Int.negSucc_ofNat_mul_negOfNat

added theorem Int.negSucc_ofNat_mul_subNatNat

added theorem Int.negSucc_ofNat_ofNat

added theorem Int.neg_neg_ofNat_succ

deleted theorem Int.neg_neg_of_nat_succ

added theorem Int.neg_ofNat_of_succ

added theorem Int.neg_ofNat_zero

deleted def Int.neg_of_nat

deleted theorem Int.neg_of_nat_add

deleted theorem Int.neg_of_nat_eq_sub_nat_nat_zero

deleted theorem Int.neg_of_nat_mul_neg_succ_of_nat

deleted theorem Int.neg_of_nat_mul_of_nat

deleted theorem Int.neg_of_nat_of_succ

deleted theorem Int.neg_of_nat_zero

deleted theorem Int.neg_succ_of_nat_add_neg_succ_of_nat

deleted theorem Int.neg_succ_of_nat_add_of_nat

deleted theorem Int.neg_succ_of_nat_coe'

deleted theorem Int.neg_succ_of_nat_coe

deleted theorem Int.neg_succ_of_nat_eq

deleted theorem Int.neg_succ_of_nat_inj_iff

deleted theorem Int.neg_succ_of_nat_mul_neg_of_nat

deleted theorem Int.neg_succ_of_nat_mul_sub_nat_nat

deleted theorem Int.neg_succ_of_nat_of_nat

deleted def Int.nonneg

added theorem Int.ofNat_add

added theorem Int.ofNat_add_negSucc_ofNat

added theorem Int.ofNat_add_ofNat

added theorem Int.ofNat_eq_ofNat_iff

added theorem Int.ofNat_mul

added theorem Int.ofNat_mul_negOfNat

added theorem Int.ofNat_mul_negSucc_ofNat

added theorem Int.ofNat_mul_ofNat

added theorem Int.ofNat_mul_subNatNat

added theorem Int.ofNat_one

added theorem Int.ofNat_sub

added theorem Int.ofNat_succ

added theorem Int.ofNat_zero

deleted theorem Int.of_nat_add

deleted theorem Int.of_nat_add_neg_succ_of_nat

deleted theorem Int.of_nat_add_of_nat

deleted theorem Int.of_nat_eq_coe

deleted theorem Int.of_nat_eq_of_nat_iff

deleted theorem Int.of_nat_mul

deleted theorem Int.of_nat_mul_neg_of_nat

deleted theorem Int.of_nat_mul_neg_succ_of_nat

deleted theorem Int.of_nat_mul_of_nat

deleted theorem Int.of_nat_mul_sub_nat_nat

deleted theorem Int.of_nat_one

deleted theorem Int.of_nat_sub

deleted theorem Int.of_nat_succ

deleted theorem Int.of_nat_zero

added theorem Int.sign_mul_natAbs

deleted theorem Int.sign_mul_nat_abs

added theorem Int.subNatNat_add

added theorem Int.subNatNat_add_add

added theorem Int.subNatNat_add_left

added theorem Int.subNatNat_add_negSucc_ofNat

added theorem Int.subNatNat_add_right

added theorem Int.subNatNat_elim

added theorem Int.subNatNat_of_le

added theorem Int.subNatNat_of_lt

added theorem Int.subNatNat_of_sub_eq_succ

added theorem Int.subNatNat_of_sub_eq_zero

added theorem Int.subNatNat_sub

deleted def Int.sub_nat_nat

deleted theorem Int.sub_nat_nat_add

deleted theorem Int.sub_nat_nat_add_add

deleted theorem Int.sub_nat_nat_add_left

deleted theorem Int.sub_nat_nat_add_neg_succ_of_nat

deleted theorem Int.sub_nat_nat_add_right

deleted theorem Int.sub_nat_nat_elim

deleted theorem Int.sub_nat_nat_of_le

deleted theorem Int.sub_nat_nat_of_lt

deleted theorem Int.sub_nat_nat_of_sub_eq_succ

deleted theorem Int.sub_nat_nat_of_sub_eq_zero

deleted theorem Int.sub_nat_nat_sub

modified theorem Int.sub_nat_self

added theorem Int.toNat_sub

deleted def Int.to_nat

deleted theorem Int.to_nat_sub

Modified Mathlib/Data/List/Card.lean

Modified Mathlib/Data/Subtype.lean

deleted theorem Subtype.coe_prop

deleted theorem Subtype.val_eq_coe

modified theorem Subtype.val_prop

Modified Mathlib/Init/Logic.lean

added theorem And.left_comm

added theorem Bool.ff_ne_tt

deleted theorem and_left_comm

deleted theorem bool.ff_ne_tt

Modified Mathlib/Logic/Basic.lean

added theorem And.congr_left_iff

added theorem And.congr_right_iff

added theorem And.imp_left

added theorem And.imp_right

added theorem And.right_comm

added theorem And.rotate

added theorem Decidable.iff_iff_not_or_and_or_not

added theorem Decidable.not_imp_self

added theorem Not.decidable_imp_symm

added theorem Not.imp_symm

added theorem Or.elim3

added theorem and_congr_left'

added theorem and_congr_left

added theorem and_congr_right'

added theorem and_iff_left_iff_imp

added theorem and_iff_left_of_imp

added theorem and_iff_not_or_not

added theorem and_iff_right_iff_imp

added theorem and_iff_right_of_imp

added theorem and_not_self_iff

added theorem and_or_distrib_left

added theorem and_or_distrib_right

added theorem and_self_left

added theorem and_self_right

added theorem by_contra

added def decidable_of_bool

added def decidable_of_iff'

modified def decidable_of_iff

added theorem iff_and_self

added theorem iff_false_left

added theorem iff_false_right

added theorem iff_iff_and_or_not_and_not

added theorem iff_iff_not_or_and_or_not

added theorem iff_mpr_iff_true_intro

added theorem iff_not_comm

added theorem iff_of_false

added theorem iff_of_true

added theorem iff_self_and

added theorem iff_true_left

added theorem iff_true_right

added theorem imp.swap

added theorem imp_iff_not_or

added theorem imp_imp_imp

added theorem imp_not_comm

added theorem imp_not_self

added theorem imp_or_distrib'

added theorem imp_or_distrib

added theorem not_and'

added theorem not_and_distrib

added theorem not_and_not_right

added theorem not_and_of_not_left

added theorem not_and_of_not_or_not

added theorem not_and_of_not_right

added theorem not_and_self_iff

added theorem not_iff

added theorem not_iff_comm

added theorem not_iff_not

added theorem not_imp

added theorem not_imp_comm

added theorem not_imp_not

added theorem not_imp_of_and_not

added theorem not_imp_self

added theorem not_not

added theorem not_or_distrib

added theorem not_or_of_imp

added theorem of_not_imp

added theorem of_not_not

deleted theorem or.elim3

added theorem or_and_distrib_left

added theorem or_and_distrib_right

added theorem or_iff_left_iff_imp

added theorem or_iff_not_and_not

added theorem or_iff_not_imp_left

added theorem or_iff_not_imp_right

added theorem or_iff_right_iff_imp

added theorem or_self_left

added theorem or_self_right

added theorem peirce'

added theorem peirce

added theorem xor_comm

added theorem xor_false

added theorem xor_self

added theorem xor_true

Created Mathlib/Tactic/Coe.lean