Commit 2022-08-31 14:18 76be8c73

View on Github →

chore(algebra/order/absolute_value): superficial tidying (#16190) This weakens the requirements of many lemmas in this file, preparing for further changes. is_absolute_value is unbundled, which is an approach that is currently not favoured in mathlib.

Estimated changes

Modified src/algebra/order/absolute_value.lean

added theorem absolute_value.map_one_of_is_regular

modified theorem is_absolute_value.abv_div

added def is_absolute_value.abv_hom'

modified def is_absolute_value.abv_hom

modified theorem is_absolute_value.abv_inv

added theorem is_absolute_value.abv_one'

modified theorem is_absolute_value.abv_one

modified theorem is_absolute_value.abv_pos

modified theorem is_absolute_value.abv_zero