Commit 2022-09-26 19:49 db24ba7c

View on Github →

chore(number_theory/padics): stylistic changes (#15755) Extracted stylistic changes (backticks, brackets, linebreaks, naming, spacing) from #15221 as suggested in the comments.

Estimated changes

Modified src/number_theory/padics/padic_integers.lean

modified theorem padic_int.exists_pow_neg_lt

modified theorem padic_int.exists_pow_neg_lt_rat

modified theorem padic_int.ideal_eq_span_pow_p

modified theorem padic_int.inv_mul

modified theorem padic_int.irreducible_p

modified theorem padic_int.mk_units_eq

modified theorem padic_int.norm_eq_of_norm_add_lt_left

modified theorem padic_int.norm_eq_of_norm_add_lt_right

modified theorem padic_int.norm_eq_padic_norm

modified theorem padic_int.norm_eq_pow_val

modified theorem padic_int.norm_int_cast_eq_padic_norm

modified theorem padic_int.norm_int_le_pow_iff_dvd

modified theorem padic_int.norm_le_pow_iff_norm_lt_pow_add_one

modified theorem padic_int.norm_lt_pow_iff_norm_le_pow_sub_one

modified theorem padic_int.norm_mul

modified theorem padic_int.norm_pow

modified theorem padic_int.norm_units

modified theorem padic_int.padic_norm_e_of_padic_int

modified theorem padic_int.valuation_one

modified theorem padic_int.valuation_p

modified theorem padic_int.valuation_zero

Modified src/number_theory/padics/padic_norm.lean

modified theorem padic_norm.padic_norm_p

modified theorem padic_norm.padic_norm_p_of_prime

modified def padic_norm

Modified src/number_theory/padics/padic_numbers.lean

modified theorem padic.add_valuation.apply

modified def padic.add_valuation_def

modified theorem padic.norm_eq_pow_val

modified theorem padic.norm_le_pow_iff_norm_lt_pow_add_one

modified theorem padic.norm_lt_pow_iff_norm_le_pow_sub_one

modified theorem padic.padic_norm_e_lim_le

modified theorem padic.rat_dense'

modified theorem padic.rat_dense

modified def padic.valuation

modified theorem padic.valuation_zero

modified theorem padic_norm_e.add_eq_max_of_ne

modified theorem padic_norm_e.eq_of_norm_add_lt_left

modified theorem padic_norm_e.eq_of_norm_add_lt_right

modified theorem padic_norm_e.eq_padic_norm

modified theorem padic_norm_e.norm_int_le_pow_iff_dvd

modified theorem padic_norm_e.norm_p_pow

modified theorem padic_seq.eq_zero_iff_equiv_zero

modified def padic_seq.norm

modified theorem padic_seq.norm_eq_pow_val

modified theorem padic_seq.norm_neg

modified theorem padic_seq.norm_nonarchimedean

modified theorem padic_seq.norm_nonzero_of_not_equiv_zero

modified theorem padic_seq.norm_values_discrete

modified theorem padic_seq.not_equiv_zero_const_of_nonzero

modified def padic_seq.stationary_point

Modified src/number_theory/padics/padic_val.lean

modified theorem dvd_of_one_le_padic_val_nat

modified theorem padic_val_int.of_nat

modified theorem padic_val_int.self

modified def padic_val_int

modified theorem padic_val_nat_dvd_iff

modified theorem padic_val_nat_primes

modified theorem padic_val_rat.le_padic_val_rat_add_of_le

modified theorem padic_val_rat.self

modified theorem padic_val_rat.sum_pos_of_pos

modified def padic_val_rat

modified theorem padic_val_rat_of_nat

modified theorem pow_padic_val_nat_dvd

modified theorem pow_succ_padic_val_nat_not_dvd

modified theorem range_pow_padic_val_nat_subset_divisors'

modified theorem range_pow_padic_val_nat_subset_divisors

Modified src/number_theory/padics/ring_homs.lean