Commit 2020-08-17 15:28 3edf2b27

View on Github →

feat(ring_theory/DVR,padics/padic_integers): characterize ideals of DVRs, apply to Z_p (#3827) Also introduce the p-adic valuation on Z_p, stolen from the perfectoid project. Coauthored by: Johan Commelin johan@commelin.net

Estimated changes

Modified src/algebra/group_power.lean

added theorem dvd_pow

Modified src/data/padics/padic_integers.lean

added theorem padic_int.ideal_eq_span_pow_p

added theorem padic_int.irreducible_p

added theorem padic_int.maximal_ideal_eq_span_p

added def padic_int.mk_units

added theorem padic_int.mk_units_eq

added theorem padic_int.norm_eq_pow_val

added theorem padic_int.norm_units

added theorem padic_int.p_dvd_of_norm_lt_one

added theorem padic_int.p_nonnunit

added theorem padic_int.prime_p

added def padic_int.unit_coeff

added theorem padic_int.unit_coeff_coe

added theorem padic_int.unit_coeff_spec

added def padic_int.valuation

added theorem padic_int.valuation_nonneg

added theorem padic_int.valuation_one

added theorem padic_int.valuation_p

added theorem padic_int.valuation_zero

added theorem padic_norm_z.norm_p

added theorem padic_norm_z.norm_p_pow

Modified src/ring_theory/discrete_valuation_ring.lean

added theorem discrete_valuation_ring.associated_pow_irreducible

added theorem discrete_valuation_ring.aux_pid_of_ufd_of_unique_irreducible

added theorem discrete_valuation_ring.has_unit_mul_pow_irreducible_factorization.of_ufd_of_unique_irreducible

added theorem discrete_valuation_ring.has_unit_mul_pow_irreducible_factorization.unique_irreducible

added def discrete_valuation_ring.has_unit_mul_pow_irreducible_factorization

added theorem discrete_valuation_ring.ideal_eq_span_pow_irreducible

deleted theorem discrete_valuation_ring.iff_PID_with_one_nonzero_prime

added theorem discrete_valuation_ring.iff_pid_with_one_nonzero_prime

deleted theorem discrete_valuation_ring.irreducible_iff_uniformiser

added theorem discrete_valuation_ring.irreducible_iff_uniformizer

added theorem discrete_valuation_ring.of_has_unit_mul_pow_irreducible_factorization

added theorem discrete_valuation_ring.of_ufd_of_unique_irreducible