Commit 2023-03-23 13:44 0d3a725b

View on Github →

feat: port NumberTheory.Zsqrtd.Basic (#3034)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Zsqrtd/Basic.lean

added theorem Zsqrtd.Nonneg.add

added def Zsqrtd.Nonneg

added def Zsqrtd.Nonnegg

added theorem Zsqrtd.Nonsquare.ns

added def Zsqrtd.SqLe

added theorem Zsqrtd.add_def

added theorem Zsqrtd.add_im

added theorem Zsqrtd.add_re

added theorem Zsqrtd.bit0_im

added theorem Zsqrtd.bit0_re

added theorem Zsqrtd.bit1_im

added theorem Zsqrtd.bit1_re

added theorem Zsqrtd.coe_int_dvd_coe_int

added theorem Zsqrtd.coe_int_dvd_iff

added theorem Zsqrtd.coe_int_im

added theorem Zsqrtd.coe_int_re

added theorem Zsqrtd.coe_int_val

added theorem Zsqrtd.coe_nat_im

added theorem Zsqrtd.coe_nat_re

added theorem Zsqrtd.coe_nat_val

added theorem Zsqrtd.coprime_of_dvd_coprime

added theorem Zsqrtd.d_pos

added theorem Zsqrtd.decompose

added theorem Zsqrtd.divides_sq_eq_zero

added theorem Zsqrtd.divides_sq_eq_zero_z

added theorem Zsqrtd.dmuld

added theorem Zsqrtd.exists_coprime_of_gcd_pos

added theorem Zsqrtd.ext

added theorem Zsqrtd.gcd_eq_zero_iff

added theorem Zsqrtd.gcd_pos_iff

added theorem Zsqrtd.hom_ext

added theorem Zsqrtd.isUnit_iff_norm_isUnit

added theorem Zsqrtd.le_antisymm

added theorem Zsqrtd.le_arch

added theorem Zsqrtd.le_of_le_le

added def Zsqrtd.lift

added theorem Zsqrtd.lift_injective

added theorem Zsqrtd.mker_norm_eq_unitary

added theorem Zsqrtd.mul_im

added theorem Zsqrtd.mul_re

added theorem Zsqrtd.mul_star

added theorem Zsqrtd.muld_val

added theorem Zsqrtd.neg_im

added theorem Zsqrtd.neg_re

added theorem Zsqrtd.nonneg_add_lem

added theorem Zsqrtd.nonneg_antisymm

added theorem Zsqrtd.nonneg_cases

added theorem Zsqrtd.nonneg_iff_zero_le

added theorem Zsqrtd.nonneg_mul

added theorem Zsqrtd.nonneg_mul_lem

added theorem Zsqrtd.nonneg_muld

added theorem Zsqrtd.nonneg_smul

added theorem Zsqrtd.nonnegg_cases_left

added theorem Zsqrtd.nonnegg_cases_right

added theorem Zsqrtd.nonnegg_comm

added theorem Zsqrtd.nonnegg_neg_pos

added theorem Zsqrtd.nonnegg_pos_neg

added def Zsqrtd.norm

added def Zsqrtd.normMonoidHom

added theorem Zsqrtd.norm_conj

added theorem Zsqrtd.norm_def

added theorem Zsqrtd.norm_eq_mul_conj

added theorem Zsqrtd.norm_eq_of_associated

added theorem Zsqrtd.norm_eq_one_iff'

added theorem Zsqrtd.norm_eq_one_iff

added theorem Zsqrtd.norm_eq_one_iff_mem_unitary

added theorem Zsqrtd.norm_eq_zero

added theorem Zsqrtd.norm_eq_zero_iff

added theorem Zsqrtd.norm_int_cast

added theorem Zsqrtd.norm_mul

added theorem Zsqrtd.norm_nat_cast

added theorem Zsqrtd.norm_neg

added theorem Zsqrtd.norm_nonneg

added theorem Zsqrtd.norm_one

added theorem Zsqrtd.norm_zero

added theorem Zsqrtd.not_divides_sq

added theorem Zsqrtd.not_sqLe_succ

added def Zsqrtd.ofInt

added theorem Zsqrtd.ofInt_eq_coe

added theorem Zsqrtd.ofInt_im

added theorem Zsqrtd.ofInt_re

added theorem Zsqrtd.one_im

added theorem Zsqrtd.one_re

added theorem Zsqrtd.smul_im

added theorem Zsqrtd.smul_re

added theorem Zsqrtd.smul_val

added theorem Zsqrtd.smuld_val

added theorem Zsqrtd.sqLe_add

added theorem Zsqrtd.sqLe_add_mixed

added theorem Zsqrtd.sqLe_cancel

added theorem Zsqrtd.sqLe_mul

added theorem Zsqrtd.sqLe_of_le

added theorem Zsqrtd.sqLe_smul

added def Zsqrtd.sqrtd

added theorem Zsqrtd.sqrtd_im

added theorem Zsqrtd.sqrtd_re

added theorem Zsqrtd.star_im

added theorem Zsqrtd.star_mk

added theorem Zsqrtd.star_re

added theorem Zsqrtd.zero_im

added theorem Zsqrtd.zero_re

added structure Zsqrtd