Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-02 17:42 8dcd0718

View on Github →

generalize norm to zsqrtd

Estimated changes

Modified src/data/gaussian_int.lean

added theorem gaussian_int.coe_nat_abs_norm

added theorem gaussian_int.nat_abs_norm_mod_lt

added theorem gaussian_int.nat_cast_nat_abs_norm

deleted def gaussian_int.norm

deleted theorem gaussian_int.norm_eq_one_iff

added theorem gaussian_int.norm_mod_lt

deleted theorem gaussian_int.norm_mul

deleted theorem gaussian_int.norm_nat_cast

added theorem gaussian_int.norm_nonneg

deleted theorem gaussian_int.norm_one

deleted theorem gaussian_int.norm_zero

Modified src/number_theory/pell.lean

added def zsqrtd.norm

added theorem zsqrtd.norm_eq_mul_conj

added theorem zsqrtd.norm_eq_one_iff

added theorem zsqrtd.norm_int_cast

added theorem zsqrtd.norm_mul

added theorem zsqrtd.norm_nat_cast

added theorem zsqrtd.norm_nonneg

added theorem zsqrtd.norm_one

added theorem zsqrtd.norm_zero

Modified src/number_theory/sum_two_squares.lean