Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-12 20:08 da4ec7e1

View on Github →

feat(ring_theory/valuation/valuation_subring): Valuation subrings of a field (#12741)

Estimated changes

Created src/ring_theory/valuation/valuation_subring.lean

added theorem valuation_subring.algebra_map_apply

added theorem valuation_subring.ext

added theorem valuation_subring.le_top

added theorem valuation_subring.mem_carrier

added theorem valuation_subring.mem_of_valuation_le_one

added theorem valuation_subring.mem_or_inv_mem

added theorem valuation_subring.mem_to_subring

added theorem valuation_subring.mem_top

added def valuation_subring.valuation

added theorem valuation_subring.valuation_eq_iff

added theorem valuation_subring.valuation_le_iff

added theorem valuation_subring.valuation_le_one

added theorem valuation_subring.valuation_le_one_iff

added theorem valuation_subring.valuation_surjective

added structure valuation_subring