Commit 2022-11-20 21:39 085e7ab4

View on Github →

feat: port Algebra.Ring.Defs (#655) Tracking mathlib commit: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

Estimated changes

deleted theorem add_mul
deleted theorem mul_add
deleted theorem mul_neg
deleted theorem mul_sub_right_distrib
deleted theorem neg_mul
deleted theorem neg_mul_eq_neg_mul
added theorem add_mul_self_eq
added theorem add_one_mul
added theorem bit0_eq_two_mul
added theorem boole_mul
added theorem distrib_three_right
added theorem ite_and_mul_zero
added theorem ite_mul
added theorem ite_mul_zero_left
added theorem ite_mul_zero_right
added theorem left_distrib
added theorem mul_add_one
added theorem mul_boole
added theorem mul_ite
added theorem mul_neg
added theorem mul_neg_one
added theorem mul_one_add
added theorem mul_one_sub
added theorem mul_sub_left_distrib
added theorem mul_sub_one
added theorem mul_sub_right_distrib
added theorem mul_two
added theorem neg_eq_neg_one_mul
added theorem neg_mul
added theorem neg_mul_comm
added theorem neg_mul_eq_mul_neg
added theorem neg_mul_eq_neg_mul
added theorem neg_mul_neg
added theorem neg_one_mul
added theorem one_add_mul
added theorem one_sub_mul
added theorem right_distrib
added theorem sub_one_mul
added theorem two_mul
added theorem one_add_one_eq_two