Commit 2020-06-10 12:50 4b622613

View on Github →

chore(algebra/field): deduplicate with group_with_zero (#3015) For historical reasons there are lots of lemmas we prove for group_with_zero, then again for a division_ring. Merge some of them.

Estimated changes

Modified src/algebra/continued_fractions/convergents_equiv.lean

Modified src/algebra/field.lean

deleted theorem div_div_div_div_eq

deleted theorem div_div_eq_div_mul

deleted theorem div_div_eq_mul_div

deleted theorem div_eq_mul_one_div

deleted theorem div_helper

deleted theorem div_mul_cancel

deleted theorem div_mul_div

deleted theorem div_mul_eq_div_mul_one_div

deleted theorem div_mul_eq_mul_div

deleted theorem div_mul_eq_mul_div_comm

deleted theorem div_mul_left

deleted theorem div_mul_right

deleted theorem div_one

deleted theorem div_self

deleted theorem division_def

deleted theorem eq_of_mul_eq_mul_of_nonzero_left

deleted theorem eq_of_mul_eq_mul_of_nonzero_right

deleted theorem eq_zero_of_one_div_eq_zero

deleted theorem inv_mul_cancel

deleted theorem inv_ne_zero

deleted theorem inv_one

deleted theorem mul_div_assoc

deleted theorem mul_div_cancel'

deleted theorem mul_div_cancel

deleted theorem mul_div_cancel_left

deleted theorem mul_div_mul_left

deleted theorem mul_div_mul_right

deleted theorem mul_eq_mul_of_div_eq_div

deleted theorem mul_inv_cancel

deleted theorem mul_one_div_cancel

deleted theorem ne_zero_of_one_div_ne_zero

deleted theorem one_div_mul_cancel

deleted theorem one_div_mul_one_div

deleted theorem one_div_ne_zero

deleted theorem one_div_one

deleted theorem one_inv_eq

deleted theorem zero_div

Modified src/algebra/group_with_zero.lean

deleted theorem div_div_div_div_eq'

added theorem div_div_div_div_eq

deleted theorem div_div_eq_div_mul'

added theorem div_div_eq_div_mul

deleted theorem div_div_eq_mul_div'

added theorem div_div_eq_mul_div

deleted theorem div_eq_mul_one_div'

added theorem div_eq_mul_one_div

deleted theorem div_helper'

added theorem div_helper

deleted theorem div_mul_cancel'

added theorem div_mul_cancel

deleted theorem div_mul_div'

added theorem div_mul_div

deleted theorem div_mul_eq_div_mul_one_div'

added theorem div_mul_eq_div_mul_one_div

deleted theorem div_mul_eq_mul_div'

added theorem div_mul_eq_mul_div

deleted theorem div_mul_eq_mul_div_comm'

added theorem div_mul_eq_mul_div_comm

deleted theorem div_mul_left'

added theorem div_mul_left

deleted theorem div_mul_right'

added theorem div_mul_right

deleted theorem div_one'

added theorem div_one

deleted theorem div_self'

added theorem div_self

deleted theorem eq_of_mul_eq_mul_of_nonzero_left'

added theorem eq_of_mul_eq_mul_of_nonzero_left

deleted theorem eq_of_mul_eq_mul_of_nonzero_right'

added theorem eq_of_mul_eq_mul_of_nonzero_right

deleted theorem eq_zero_of_one_div_eq_zero'

added theorem eq_zero_of_one_div_eq_zero

deleted theorem inv_mul_cancel'

added theorem inv_mul_cancel

deleted theorem inv_ne_zero'

added theorem inv_ne_zero

deleted theorem inv_one'

added theorem inv_one

deleted theorem mul_div_assoc''

added theorem mul_div_assoc

deleted theorem mul_div_cancel'''

deleted theorem mul_div_cancel''

added theorem mul_div_cancel'

added theorem mul_div_cancel

deleted theorem mul_div_cancel_left'

added theorem mul_div_cancel_left

deleted theorem mul_div_mul_left'

added theorem mul_div_mul_left

deleted theorem mul_div_mul_right'

added theorem mul_div_mul_right

deleted theorem mul_eq_mul_of_div_eq_div'

added theorem mul_eq_mul_of_div_eq_div

deleted theorem mul_inv_cancel'

added theorem mul_inv_cancel

deleted theorem mul_one_div_cancel'

added theorem mul_one_div_cancel

deleted theorem ne_zero_of_one_div_ne_zero'

added theorem ne_zero_of_one_div_ne_zero

deleted theorem one_div_mul_cancel'

added theorem one_div_mul_cancel

deleted theorem one_div_mul_one_div'

added theorem one_div_mul_one_div

deleted theorem one_div_ne_zero'

added theorem one_div_ne_zero

deleted theorem one_div_one'

added theorem one_div_one

added theorem one_inv_eq

deleted theorem zero_div'

added theorem zero_div

Modified src/algebra/group_with_zero_power.lean

Modified src/algebra/invertible.lean

Modified src/data/real/nnreal.lean

Modified src/geometry/euclidean.lean