Commit 2024-07-24 08:31 0ccc5ae5

View on Github →

chore (Algebra.Order.Group.Abs): split file into unbundled and bundled material (#15065) Currently Algebra.Order.Group.Abs imports OrderedCommMonoid and other bundled algebra classes despite much of the file using unbundled ordered algebra typeclasses. We split into Algebra.Order.Group.Unbundled.Abs and Algebra.Order.Group.Abs to separate the bundled and unbundled parts of the file and minimize imports downstream.

Estimated changes

deleted theorem Pi.abs_apply
deleted theorem Pi.abs_def
deleted def abs.unexpander
deleted theorem eq_or_eq_inv_of_mabs_eq
deleted theorem inv_le_mabs
deleted theorem inv_lt_of_mabs_lt
deleted theorem inv_mabs_le
deleted theorem inv_mabs_le_inv
deleted theorem isSquare_mabs
deleted theorem le_mabs
deleted theorem le_mabs_self
deleted theorem lt_mabs
deleted theorem lt_of_mabs_lt
deleted theorem m_Birkhoff_inequalities
deleted def mabs.unexpander
deleted def mabs
deleted theorem mabs_by_cases
deleted theorem mabs_choice
deleted theorem mabs_div_comm
deleted theorem mabs_eq_mabs
deleted theorem mabs_eq_max_inv
deleted theorem mabs_eq_one
deleted theorem mabs_inf_div_inf_le_mabs
deleted theorem mabs_inv
deleted theorem mabs_le'
deleted theorem mabs_le_mabs
deleted theorem mabs_le_mabs_of_le_one
deleted theorem mabs_le_mabs_of_one_le
deleted theorem mabs_le_one
deleted theorem mabs_lt
deleted theorem mabs_mabs
deleted theorem mabs_mabs_div_mabs_le
deleted theorem mabs_mul_le
deleted theorem mabs_ne_one
deleted theorem mabs_of_le_one
deleted theorem mabs_of_lt_one
deleted theorem mabs_of_one_le
deleted theorem mabs_of_one_lt
deleted theorem mabs_one
deleted theorem mabs_sup_div_sup_le_mabs
deleted theorem max_div_min_eq_mabs'
deleted theorem max_div_min_eq_mabs
deleted theorem one_le_mabs
deleted theorem one_le_mul_mabs
deleted theorem one_lt_mabs
deleted theorem one_lt_mabs_of_lt_one
deleted theorem one_lt_mabs_pos_of_one_lt
deleted theorem sup_div_inf_eq_mabs_div
added theorem Pi.abs_apply
added theorem Pi.abs_def
added def abs.unexpander
added theorem inv_le_mabs
added theorem inv_lt_of_mabs_lt
added theorem inv_mabs_le
added theorem inv_mabs_le_inv
added theorem isSquare_mabs
added theorem le_mabs
added theorem le_mabs_self
added theorem lt_mabs
added theorem lt_of_mabs_lt
added def mabs.unexpander
added def mabs
added theorem mabs_by_cases
added theorem mabs_choice
added theorem mabs_div_comm
added theorem mabs_eq_mabs
added theorem mabs_eq_max_inv
added theorem mabs_eq_one
added theorem mabs_inv
added theorem mabs_le'
added theorem mabs_le_mabs
added theorem mabs_le_mabs_of_le_one
added theorem mabs_le_mabs_of_one_le
added theorem mabs_le_one
added theorem mabs_lt
added theorem mabs_mabs
added theorem mabs_mabs_div_mabs_le
added theorem mabs_mul_le
added theorem mabs_ne_one
added theorem mabs_of_le_one
added theorem mabs_of_lt_one
added theorem mabs_of_one_le
added theorem mabs_of_one_lt
added theorem mabs_one
added theorem max_div_min_eq_mabs'
added theorem max_div_min_eq_mabs
added theorem one_le_mabs
added theorem one_le_mul_mabs
added theorem one_lt_mabs
added theorem one_lt_mabs_of_lt_one