GaussianInt

📁 Source: Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean

Statistics

Metric	Count
Definitions GaussianInt, instCoeComplex, instCommRing, instDiv, instEuclideanDomain, instMod, instRepr, toComplex	8
Theorems abs_natCast_norm, div_def, im_toComplex, instNontrivial, intCast_complex_norm, intCast_im, intCast_re, intCast_real_norm, mod_def, natAbs_norm_eq, natAbs_norm_mod_lt, natCast_natAbs_norm, normSq_div_sub_div_lt_one, normSq_le_normSq_of_re_le_of_im_le, norm_eq_zero, norm_le_norm_mul_left, norm_mod_lt, norm_nonneg, norm_pos, re_toComplex, sq_add_sq_of_nat_prime_of_not_irreducible, toComplex_add, toComplex_def, toComplex_def', toComplex_def₂, toComplex_div_im, toComplex_div_re, toComplex_eq_zero, toComplex_im, toComplex_im_div, toComplex_inj, toComplex_injective, toComplex_mul, toComplex_neg, toComplex_one, toComplex_re, toComplex_re_div, toComplex_star, toComplex_sub, toComplex_zero, to_real_im, to_real_re	42
Total	50

GaussianInt

Definitions

Name	Category	Theorems
instCoeComplex 📖	CompOp	—
instCommRing 📖	CompOp	—
instDiv 📖	CompOp	7 math math: toComplex_div_re, toComplex_im_div, div_def, toComplex_re_div, mod_def, normSq_div_sub_div_lt_one, toComplex_div_im
instEuclideanDomain 📖	CompOp	—
instMod 📖	CompOp	3 math math: natAbs_norm_mod_lt, norm_mod_lt, mod_def
instRepr 📖	CompOp	—
toComplex 📖	CompOp	28 math math: toComplex_mul, intCast_im, toComplex_def', toComplex_def₂, toComplex_div_re, toComplex_injective, toComplex_im_div, toComplex_add, toComplex_sub, toComplex_star, toComplex_def, to_real_re, to_real_im, toComplex_re_div, toComplex_re, toComplex_inj, intCast_real_norm, toComplex_im, im_toComplex, toComplex_neg, re_toComplex, toComplex_zero, toComplex_one, normSq_div_sub_div_lt_one, intCast_complex_norm, intCast_re, toComplex_div_im, toComplex_eq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_natCast_norm 📖	mathematical	—	Zsqrtd.norm	—	norm_nonneg
div_def 📖	mathematical	—	GaussianInt instDiv round DivisionRing.toRing Rat.instDivisionRing Rat.linearOrder Rat.instFloorRing Zsqrtd.re Zsqrtd.instMul Star.star Zsqrtd.instStar Zsqrtd.norm Zsqrtd.im	—	neg_mul one_mul mul_neg neg_neg Int.cast_add Int.cast_mul Int.cast_neg div_eq_mul_inv
im_toComplex 📖	mathematical	—	Complex.im DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex Real Real.instIntCast	—	mul_one MulZeroClass.mul_zero add_zero zero_add
instNontrivial 📖	mathematical	—	Nontrivial GaussianInt	—	—
intCast_complex_norm 📖	mathematical	—	Complex Complex.instIntCast Zsqrtd.norm Complex.ofReal DFunLike.coe MonoidWithZeroHom Real NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Complex.instSemiring Real.semiring MonoidWithZeroHom.funLike Complex.normSq RingHom GaussianInt Zsqrtd.instSemiring RingHom.instFunLike toComplex	—	Zsqrtd.norm.eq_1 Complex.normSq.eq_1 neg_mul one_mul sub_neg_eq_add Int.cast_add Int.cast_mul re_toComplex im_toComplex Complex.ofReal_add Complex.ofReal_mul
intCast_im 📖	mathematical	—	Real Real.instIntCast Zsqrtd.im Complex.im DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex	—	mul_one MulZeroClass.mul_zero add_zero zero_add
intCast_re 📖	mathematical	—	Real Real.instIntCast Zsqrtd.re Complex.re DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex	—	MulZeroClass.mul_zero mul_one sub_self add_zero
intCast_real_norm 📖	mathematical	—	Real Real.instIntCast Zsqrtd.norm DFunLike.coe MonoidWithZeroHom Complex NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Complex.instSemiring Real.semiring MonoidWithZeroHom.funLike Complex.normSq RingHom GaussianInt Zsqrtd.instSemiring RingHom.instFunLike toComplex	—	Zsqrtd.norm.eq_1 Complex.normSq.eq_1 neg_mul one_mul sub_neg_eq_add Int.cast_add Int.cast_mul intCast_re intCast_im
mod_def 📖	mathematical	—	GaussianInt instMod SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Zsqrtd.addGroupWithOne Zsqrtd.instMul instDiv	—	—
natAbs_norm_eq 📖	mathematical	—	Zsqrtd.norm Zsqrtd.re Zsqrtd.im	—	Int.natCast_natAbs Nat.cast_add Nat.cast_mul Zsqrtd.abs_norm Int.instAddLeftMono Int.instZeroLEOneClass neg_mul one_mul sub_neg_eq_add abs_mul_abs_self
natAbs_norm_mod_lt 📖	mathematical	—	Zsqrtd.norm GaussianInt instMod	—	Nat.cast_natAbs Zsqrtd.abs_norm Int.instAddLeftMono Int.instZeroLEOneClass norm_mod_lt
natCast_natAbs_norm 📖	mathematical	—	AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Zsqrtd.norm AddGroupWithOne.toIntCast	—	Nat.cast_natAbs Zsqrtd.abs_norm Int.instAddLeftMono Int.instZeroLEOneClass
normSq_div_sub_div_lt_one 📖	mathematical	—	Real Real.instLT DFunLike.coe MonoidWithZeroHom Complex NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Complex.instSemiring Real.semiring MonoidWithZeroHom.funLike Complex.normSq Complex.instSub DivInvMonoid.toDiv Complex.instDivInvMonoid RingHom GaussianInt Zsqrtd.instSemiring RingHom.instFunLike toComplex instDiv Real.instOne	—	Nat.instAtLeastTwoHAddOfNat Complex.ext MulZeroClass.mul_zero sub_self mul_one add_zero zero_add abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instIsOrderedRing normSq_le_normSq_of_re_le_of_im_le toComplex_re_div one_div Complex.inv_re div_self_mul_self' Complex.inv_im neg_zero zero_div abs_sub_round toComplex_im_div Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one
normSq_le_normSq_of_re_le_of_im_le 📖	mathematical	Real Real.instLE abs Real.lattice Real.instAddGroup Complex.re Complex.im	DFunLike.coe MonoidWithZeroHom Complex NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Complex.instSemiring Real.semiring MonoidWithZeroHom.funLike Complex.normSq	—	Complex.normSq_apply abs_mul_self Real.instIsOrderedRing abs_mul add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add mul_le_mul IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono abs_nonneg
norm_eq_zero 📖	mathematical	—	Zsqrtd.norm GaussianInt Zsqrtd.instZero	—	IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing intCast_real_norm Int.cast_zero Real.instNontrivial MonoidWithZeroHom.monoidWithZeroHomClass
norm_le_norm_mul_left 📖	mathematical	—	Zsqrtd.norm GaussianInt Zsqrtd.instMul	—	Zsqrtd.norm_mul le_mul_of_one_le_right IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing abs_natCast_norm norm_pos
norm_mod_lt 📖	mathematical	—	Zsqrtd.norm GaussianInt instMod	—	toComplex_zero Int.cast_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing intCast_real_norm map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Complex.normSq_mul mul_sub mul_div_cancel₀ mul_lt_mul_of_pos_left IsStrictOrderedRing.toPosMulStrictMono normSq_div_sub_div_lt_one Complex.normSq_pos mul_one
norm_nonneg 📖	mathematical	—	Zsqrtd.norm	—	Zsqrtd.norm_nonneg Int.instAddLeftMono Int.instZeroLEOneClass
norm_pos 📖	mathematical	—	Zsqrtd.norm	—	lt_iff_le_and_ne norm_eq_zero
re_toComplex 📖	mathematical	—	Complex.re DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex Real Real.instIntCast	—	MulZeroClass.mul_zero mul_one sub_self add_zero
sq_add_sq_of_nat_prime_of_not_irreducible 📖	mathematical	Irreducible GaussianInt Zsqrtd.instMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Zsqrtd.addGroupWithOne	Monoid.toNatPow Nat.instMonoid	—	Zsqrtd.norm_eq_one_iff Zsqrtd.norm_natCast mul_eq_one Unique.instSubsingleton ne_of_lt Nat.Prime.one_lt Fact.out Nat.Prime.mul_eq_prime_sq_iff sq Nat.cast_mul Nat.cast_natAbs Zsqrtd.abs_norm Int.instAddLeftMono Int.instZeroLEOneClass Zsqrtd.norm_mul natAbs_norm_eq
toComplex_add 📖	mathematical	—	DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex Zsqrtd.instAdd Complex.instAdd	—	RingHom.map_add
toComplex_def 📖	mathematical	—	DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex Complex.instAdd Complex.instIntCast Zsqrtd.re Complex.instMul Zsqrtd.im Complex.I	—	—
toComplex_def' 📖	mathematical	—	DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex Complex.instAdd Complex.instIntCast Complex.instMul Complex.I	—	—
toComplex_def₂ 📖	mathematical	—	DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex Real Real.instIntCast Zsqrtd.re Zsqrtd.im	—	Complex.ext MulZeroClass.mul_zero mul_one sub_self add_zero zero_add
toComplex_div_im 📖	mathematical	—	Complex.im DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex instDiv Real Real.instIntCast round Real.instRing Real.linearOrder Real.instFloorRing DivInvMonoid.toDiv Complex.instDivInvMonoid	—	toComplex_im_div
toComplex_div_re 📖	mathematical	—	Complex.re DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex instDiv Real Real.instIntCast round Real.instRing Real.linearOrder Real.instFloorRing DivInvMonoid.toDiv Complex.instDivInvMonoid	—	toComplex_re_div
toComplex_eq_zero 📖	mathematical	—	DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex Complex.instZero Zsqrtd.instZero	—	toComplex_zero
toComplex_im 📖	mathematical	—	Complex.im DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex Real Real.instIntCast	—	im_toComplex
toComplex_im_div 📖	mathematical	—	Complex.im DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex instDiv Real Real.instIntCast round Real.instRing Real.linearOrder Real.instFloorRing DivInvMonoid.toDiv Complex.instDivInvMonoid	—	div_def Rat.round_cast Real.instIsStrictOrderedRing neg_mul one_mul mul_neg neg_neg Int.cast_add Int.cast_mul div_eq_mul_inv add_mul Distrib.rightDistribClass mul_assoc Rat.cast_add IsStrictOrderedRing.toCharZero Rat.cast_mul Rat.cast_intCast intCast_re Rat.cast_inv intCast_real_norm intCast_im Int.cast_neg Rat.cast_neg im_toComplex Complex.inv_im Complex.inv_re
toComplex_inj 📖	mathematical	—	DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex	—	toComplex_def₂ IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
toComplex_injective 📖	mathematical	—	GaussianInt Complex DFunLike.coe RingHom Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex	—	—
toComplex_mul 📖	mathematical	—	DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex Zsqrtd.instMul Complex.instMul	—	RingHom.map_mul
toComplex_neg 📖	mathematical	—	DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex Zsqrtd.instNeg Complex.instNeg	—	RingHom.map_neg
toComplex_one 📖	mathematical	—	DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex Zsqrtd.instOne Complex.instOne	—	RingHom.map_one
toComplex_re 📖	mathematical	—	Complex.re DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex Real Real.instIntCast	—	re_toComplex
toComplex_re_div 📖	mathematical	—	Complex.re DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex instDiv Real Real.instIntCast round Real.instRing Real.linearOrder Real.instFloorRing DivInvMonoid.toDiv Complex.instDivInvMonoid	—	div_def Rat.round_cast Real.instIsStrictOrderedRing neg_mul one_mul mul_neg neg_neg Int.cast_add Int.cast_mul div_eq_mul_inv add_mul Distrib.rightDistribClass mul_assoc Rat.cast_add IsStrictOrderedRing.toCharZero Rat.cast_mul Rat.cast_intCast intCast_re Rat.cast_inv intCast_real_norm intCast_im Int.cast_neg re_toComplex Complex.inv_re Complex.inv_im sub_neg_eq_add
toComplex_star 📖	mathematical	—	DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex Star.star Zsqrtd.instStar CommSemiring.toSemiring Complex.instCommSemiring starRingEnd Complex.instStarRing	—	toComplex_def₂ Int.cast_neg
toComplex_sub 📖	mathematical	—	DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Zsqrtd.addGroupWithOne Complex.instSub	—	RingHom.map_sub
toComplex_zero 📖	mathematical	—	DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex Zsqrtd.instZero Complex.instZero	—	RingHom.map_zero
to_real_im 📖	mathematical	—	Real Real.instIntCast Zsqrtd.im Complex.im DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex	—	intCast_im
to_real_re 📖	mathematical	—	Real Real.instIntCast Zsqrtd.re Complex.re DFunLike.coe RingHom GaussianInt Complex Semiring.toNonAssocSemiring Zsqrtd.instSemiring Complex.instSemiring RingHom.instFunLike toComplex	—	intCast_re

(root)

Definitions

Name	Category	Theorems
GaussianInt 📖	CompOp	37 math math: GaussianInt.toComplex_mul, GaussianInt.intCast_im, GaussianInt.toComplex_def', GaussianInt.toComplex_def₂, GaussianInt.toComplex_div_re, GaussianInt.norm_eq_zero, GaussianInt.toComplex_injective, GaussianInt.natAbs_norm_mod_lt, GaussianInt.norm_le_norm_mul_left, GaussianInt.toComplex_im_div, GaussianInt.toComplex_add, GaussianInt.toComplex_sub, GaussianInt.toComplex_star, GaussianInt.toComplex_def, GaussianInt.to_real_re, GaussianInt.div_def, GaussianInt.to_real_im, GaussianInt.toComplex_re_div, GaussianInt.toComplex_re, GaussianInt.toComplex_inj, GaussianInt.intCast_real_norm, GaussianInt.norm_mod_lt, GaussianInt.toComplex_im, GaussianInt.im_toComplex, GaussianInt.toComplex_neg, GaussianInt.re_toComplex, GaussianInt.toComplex_zero, GaussianInt.prime_of_nat_prime_of_mod_four_eq_three, GaussianInt.instNontrivial, GaussianInt.mod_def, GaussianInt.prime_iff_mod_four_eq_three_of_nat_prime, GaussianInt.toComplex_one, GaussianInt.normSq_div_sub_div_lt_one, GaussianInt.intCast_complex_norm, GaussianInt.intCast_re, GaussianInt.toComplex_div_im, GaussianInt.toComplex_eq_zero

---

← Back to Index