Commit 2023-03-17 12:44 a9138cdb

View on Github →

feat: port RingTheory.Valuation.Basic (#2846)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Valuation/Basic.lean

added theorem AddValuation.IsEquiv.comap

added theorem AddValuation.IsEquiv.map

added theorem AddValuation.IsEquiv.ne_top

added theorem AddValuation.IsEquiv.of_eq

added theorem AddValuation.IsEquiv.refl

added theorem AddValuation.IsEquiv.symm

added theorem AddValuation.IsEquiv.trans

added theorem AddValuation.IsEquiv.val_eq

added def AddValuation.IsEquiv

added def AddValuation.asFun

added def AddValuation.comap

added theorem AddValuation.comap_comp

added theorem AddValuation.comap_id

added theorem AddValuation.ext

added theorem AddValuation.ext_iff

added def AddValuation.map

added theorem AddValuation.map_add'

added theorem AddValuation.map_add

added theorem AddValuation.map_add_of_distinct_val

added theorem AddValuation.map_add_supp

added theorem AddValuation.map_eq_of_lt_sub

added theorem AddValuation.map_inv

added theorem AddValuation.map_le_add

added theorem AddValuation.map_le_sub

added theorem AddValuation.map_le_sum

added theorem AddValuation.map_lt_add

added theorem AddValuation.map_lt_sum'

added theorem AddValuation.map_lt_sum

added theorem AddValuation.map_mul

added theorem AddValuation.map_neg

added theorem AddValuation.map_one

added theorem AddValuation.map_pow

added theorem AddValuation.map_sub

added theorem AddValuation.map_sub_swap

added theorem AddValuation.map_zero

added theorem AddValuation.mem_supp_iff

added theorem AddValuation.ne_top_iff

added def AddValuation.of

added theorem AddValuation.of_apply

added def AddValuation.supp

added def AddValuation.toPreorder

added theorem AddValuation.top_iff

added def AddValuation.valuation

added theorem AddValuation.valuation_apply

added def AddValuation

added theorem Valuation.IsEquiv.comap

added theorem Valuation.IsEquiv.map

added theorem Valuation.IsEquiv.ne_zero

added theorem Valuation.IsEquiv.of_eq

added theorem Valuation.IsEquiv.refl

added theorem Valuation.IsEquiv.symm

added theorem Valuation.IsEquiv.trans

added theorem Valuation.IsEquiv.val_eq

added def Valuation.IsEquiv

added theorem Valuation.IsEquiv_iff_val_eq_one

added theorem Valuation.IsEquiv_iff_val_le_one

added theorem Valuation.IsEquiv_iff_val_lt_one

added theorem Valuation.IsEquiv_iff_val_sub_one_lt_one

added theorem Valuation.IsEquiv_of_map_strictMono

added theorem Valuation.IsEquiv_of_val_le_one

added theorem Valuation.IsEquiv_tFAE

added theorem Valuation.coe_coe

added def Valuation.comap

added theorem Valuation.comap_apply

added theorem Valuation.comap_comp

added theorem Valuation.comap_id

added theorem Valuation.comap_supp

added theorem Valuation.ext

added theorem Valuation.ext_iff

added def Valuation.ltAddSubgroup

added def Valuation.map

added theorem Valuation.map_add'

added theorem Valuation.map_add

added theorem Valuation.map_add_eq_of_lt_left

added theorem Valuation.map_add_eq_of_lt_right

added theorem Valuation.map_add_le

added theorem Valuation.map_add_lt

added theorem Valuation.map_add_of_distinct_val

added theorem Valuation.map_add_supp

added theorem Valuation.map_eq_of_sub_lt

added theorem Valuation.map_mul

added theorem Valuation.map_neg

added theorem Valuation.map_one

added theorem Valuation.map_one_add_of_lt

added theorem Valuation.map_one_sub_of_lt

added theorem Valuation.map_pow

added theorem Valuation.map_sub

added theorem Valuation.map_sub_le

added theorem Valuation.map_sub_swap

added theorem Valuation.map_sum_le

added theorem Valuation.map_sum_lt'

added theorem Valuation.map_sum_lt

added theorem Valuation.map_zero

added theorem Valuation.mem_supp_iff

added theorem Valuation.ne_zero_iff

added theorem Valuation.one_lt_val_iff

added def Valuation.supp

added theorem Valuation.toFun_eq_coe

added theorem Valuation.toMonoidWithZeroHom_coe_eq_coe

added def Valuation.toPreorder

added theorem Valuation.unit_map_eq

added theorem Valuation.zero_iff

added structure Valuation