Commit 2023-06-22 07:23 8a76b3e5

View on Github →

feat: port NumberTheory.Zsqrtd.GaussianInt (#5134)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Complex/Basic.lean

Created Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean

added theorem GaussianInt.abs_coe_nat_norm

added theorem GaussianInt.div_def

added theorem GaussianInt.int_cast_complex_norm

added theorem GaussianInt.int_cast_real_norm

added theorem GaussianInt.mod_def

added theorem GaussianInt.natAbs_norm_eq

added theorem GaussianInt.natAbs_norm_mod_lt

added theorem GaussianInt.nat_cast_natAbs_norm

added theorem GaussianInt.normSq_div_sub_div_lt_one

added theorem GaussianInt.normSq_le_normSq_of_re_le_of_im_le

added theorem GaussianInt.norm_eq_zero

added theorem GaussianInt.norm_le_norm_mul_left

added theorem GaussianInt.norm_mod_lt

added theorem GaussianInt.norm_nonneg

added theorem GaussianInt.norm_pos

added theorem GaussianInt.sq_add_sq_of_nat_prime_of_not_irreducible

added def GaussianInt.toComplex

added theorem GaussianInt.toComplex_add

added theorem GaussianInt.toComplex_def'

added theorem GaussianInt.toComplex_def

added theorem GaussianInt.toComplex_def₂

added theorem GaussianInt.toComplex_div_im

added theorem GaussianInt.toComplex_div_re

added theorem GaussianInt.toComplex_eq_zero

added theorem GaussianInt.toComplex_im

added theorem GaussianInt.toComplex_inj

added theorem GaussianInt.toComplex_mul

added theorem GaussianInt.toComplex_neg

added theorem GaussianInt.toComplex_one

added theorem GaussianInt.toComplex_re

added theorem GaussianInt.toComplex_star

added theorem GaussianInt.toComplex_sub

added theorem GaussianInt.toComplex_zero

added theorem GaussianInt.to_real_im

added theorem GaussianInt.to_real_re

added def GaussianInt