Commit 2023-04-07 09:57 6ccf3684

View on Github →

feat: port RingTheory.Valuation.Quotient (#3322)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Valuation/Quotient.lean

added theorem AddValuation.comap_onQuot_eq

added theorem AddValuation.comap_supp

added def AddValuation.onQuot

added def AddValuation.onQuotVal

added theorem AddValuation.onQuot_comap_eq

added theorem AddValuation.self_le_supp_comap

added theorem AddValuation.supp_quot

added theorem AddValuation.supp_quot_supp

added theorem Valuation.comap_onQuot_eq

added def Valuation.onQuot

added def Valuation.onQuotVal

added theorem Valuation.onQuot_comap_eq

added theorem Valuation.self_le_supp_comap

added theorem Valuation.supp_quot

added theorem Valuation.supp_quot_supp