Commit 2024-03-19 14:54 8ff9aa61

View on Github →

chore: Move GroupWithZero lemmas earlier (#10919) Move from Algebra.GroupWithZero.Units.Lemmas to Algebra.GroupWithZero.Units.Basic the lemmas that can be moved.

Estimated changes

added theorem div_div_cancel'
added theorem div_div_cancel_left'
added theorem div_eq_div_iff
added theorem div_eq_iff
added theorem div_eq_iff_mul_eq
added theorem div_eq_of_eq_mul
added theorem div_eq_one_iff_eq
added theorem div_helper
added theorem div_left_inj'
added theorem div_mul_cancel
added theorem div_mul_cancel_of_imp
added theorem div_mul_div_cancel
added theorem div_mul_left
added theorem div_mul_right
added theorem div_self
added theorem divp_mk0
added theorem eq_div_iff
added theorem eq_div_iff_mul_eq
added theorem eq_div_of_mul_eq
added theorem inv_mul_eq_one₀
added theorem mul_div_cancel'
added theorem mul_div_cancel
added theorem mul_div_cancel_left
added theorem mul_div_cancel_of_imp'
added theorem mul_div_cancel_of_imp
added theorem mul_div_mul_left
added theorem mul_div_mul_right
added theorem mul_inv_eq_one₀
added theorem mul_mul_div
added theorem mul_one_div_cancel
added theorem one_div_mul_cancel
deleted theorem div_div_cancel'
deleted theorem div_div_cancel_left'
deleted theorem div_div_div_cancel_left'
deleted theorem div_div_div_cancel_right
deleted theorem div_eq_div_iff
deleted theorem div_eq_iff
deleted theorem div_eq_iff_mul_eq
deleted theorem div_eq_of_eq_mul
deleted theorem div_eq_one_iff_eq
deleted theorem div_helper
deleted theorem div_left_inj'
deleted theorem div_mul_cancel
deleted theorem div_mul_cancel_of_imp
deleted theorem div_mul_div_cancel
deleted theorem div_mul_left
deleted theorem div_mul_right
deleted theorem div_self
deleted theorem divp_mk0
deleted theorem eq_div_iff
deleted theorem eq_div_iff_mul_eq
deleted theorem eq_div_of_mul_eq
deleted theorem eq_inv_mul_iff_mul_eq₀
deleted theorem eq_mul_inv_iff_mul_eq₀
deleted theorem eq_mul_of_inv_mul_eq₀
deleted theorem eq_mul_of_mul_inv_eq₀
deleted theorem inv_mul_eq_iff_eq_mul₀
deleted theorem inv_mul_eq_one₀
deleted theorem mul_div_cancel'
deleted theorem mul_div_cancel
deleted theorem mul_div_cancel_left
deleted theorem mul_div_cancel_of_imp'
deleted theorem mul_div_cancel_of_imp
deleted theorem mul_div_mul_left
deleted theorem mul_div_mul_right
deleted theorem mul_eq_mul_of_div_eq_div
deleted theorem mul_eq_of_eq_inv_mul₀
deleted theorem mul_eq_of_eq_mul_inv₀
deleted theorem mul_eq_one_iff_eq_inv₀
deleted theorem mul_eq_one_iff_inv_eq₀
deleted theorem mul_inv_eq_iff_eq_mul₀
deleted theorem mul_inv_eq_one₀
deleted theorem mul_mul_div
deleted theorem mul_one_div_cancel
deleted theorem one_div_mul_cancel