Commit 2022-11-25 16:37 79c0d384

View on Github →

feat: port Algebra.GroupWithZero.Basic (#669) Tracking mathlib commit: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

Estimated changes

added theorem div_div_self
added theorem div_mul_eq_mul_div₀
added theorem div_self_mul_self'
added theorem div_self_mul_self
added theorem div_zero
added theorem eq_of_zero_eq_one
added theorem eq_zero_of_zero_eq_one
added theorem inv_eq_zero
added theorem inv_mul_cancel
added theorem inv_mul_cancel_left₀
added theorem inv_mul_mul_self
added theorem inv_ne_zero
added theorem left_ne_zero_of_mul
added theorem mul_eq_mul_left_iff
added theorem mul_eq_mul_right_iff
added theorem mul_inv_cancel_left₀
added theorem mul_inv_mul_self
added theorem mul_left_eq_self₀
added theorem mul_left_inj'
added theorem mul_left_surjective₀
added theorem mul_ne_zero
added theorem mul_right_eq_self₀
added theorem mul_right_inj'
added theorem mul_self_div_self
added theorem mul_self_mul_inv
added theorem mul_zero_eq_const
added theorem one_div_ne_zero
added theorem right_ne_zero_of_mul
added theorem zero_div
added theorem zero_eq_inv
added theorem zero_mul_eq_const
deleted theorem mul_ne_zero