Basic

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

Statistics

Metric	Count
Definitions `Zsqrtd`, `Nonneg`, `Nonnegg`, `Nonsquare`, `SqLe`, `addCommGroup`, `addGroupWithOne`, `commRing`, `decidableLE`, `decidableNonneg`, `decidableNonnegg`, `im`, `instAdd`, `instAddCommSemigroup`, `instAddMonoid`, `instAddSemigroup`, `instCommMonoid`, `instCommSemigroup`, `instCommSemiring`, `instDistrib`, `instInhabited`, `instLECastInt`, `instLTCastInt`, `instMonoid`, `instMul`, `instNeg`, `instOne`, `instRing`, `instSemigroup`, `instSemiring`, `instStar`, `instStarRing`, `instZero`, `linearOrder`, `norm`, `normMonoidHom`, `ofInt`, `preorder`, `re`, `sqrtd`, `instDecidableEqZsqrtd`, `decEq`, `«termℤ√_»`	43
Theorems `add`, `ns`, `ns'`, `abs_norm`, `add_def`, `add_im`, `add_le_add_left`, `add_lt_add_left`, `add_re`, `d_pos`, `decompose`, `divides_sq_eq_zero`, `divides_sq_eq_zero_z`, `dmuld`, `eq_of_smul_eq_smul_left`, `eq_zero_or_eq_zero_of_mul_eq_zero`, `exists_coprime_of_gcd_pos`, `ext`, `ext_iff`, `gcd_eq_zero_iff`, `gcd_pos_iff`, `hom_ext`, `hom_ext_iff`, `im_add`, `im_intCast`, `im_mul`, `im_natCast`, `im_neg`, `im_ofInt`, `im_ofNat`, `im_one`, `im_smul`, `im_sqrtd`, `im_star`, `im_sub`, `im_zero`, `instCharZero`, `instIsDomainCastInt`, `instIsOrderedAddMonoidCastInt`, `instIsStrictOrderedRingCastInt`, `instNoZeroDivisorsCastInt`, `instZeroLEOneClassCastInt`, `intCast_dvd`, `intCast_dvd_intCast`, `intCast_im`, `intCast_re`, `intCast_val`, `isCoprime_of_dvd_isCoprime`, `isUnit_iff_norm_isUnit`, `le_antisymm`, `le_arch`, `le_of_add_le_add_left`, `le_of_le_le`, `le_total`, `lift_apply_apply`, `lift_injective`, `lift_symm_apply_coe`, `mker_norm_eq_unitary`, `mul_im`, `mul_nonneg`, `mul_pos`, `mul_re`, `mul_star`, `muld_val`, `natCast_im`, `natCast_re`, `natCast_val`, `neg_im`, `neg_re`, `nonneg_add_lem`, `nonneg_antisymm`, `nonneg_cases`, `nonneg_iff_zero_le`, `nonneg_mul`, `nonneg_mul_lem`, `nonneg_muld`, `nonneg_smul`, `nonneg_total`, `nonnegg_cases_left`, `nonnegg_cases_right`, `nonnegg_comm`, `nonnegg_neg_pos`, `nonnegg_pos_neg`, `nontrivial`, `norm_conj`, `norm_def`, `norm_eq_mul_conj`, `norm_eq_of_associated`, `norm_eq_one_iff`, `norm_eq_one_iff'`, `norm_eq_one_iff_mem_unitary`, `norm_eq_zero`, `norm_eq_zero_iff`, `norm_intCast`, `norm_mul`, `norm_natCast`, `norm_neg`, `norm_nonneg`, `norm_one`, `norm_zero`, `not_divides_sq`, `not_sqLe_succ`, `nsmul_val`, `ofInt_eq_intCast`, `ofInt_im`, `ofInt_re`, `ofNat_im`, `ofNat_re`, `one_im`, `one_re`, `re_add`, `re_intCast`, `re_mul`, `re_natCast`, `re_neg`, `re_ofInt`, `re_ofNat`, `re_one`, `re_smul`, `re_sqrtd`, `re_star`, `re_sub`, `re_zero`, `smul_im`, `smul_re`, `smul_val`, `smuld_val`, `sqLe_add`, `sqLe_add_mixed`, `sqLe_cancel`, `sqLe_mul`, `sqLe_of_le`, `sqLe_smul`, `sqrtd_im`, `sqrtd_re`, `star_im`, `star_mk`, `star_re`, `sub_im`, `sub_re`, `zero_im`, `zero_re`	142
Total	185

Zsqrtd

Definitions

Name	Category	Theorems
`Nonneg` 📖	MathDef	2 math math: `nonneg_total`, `nonneg_iff_zero_le`
`Nonnegg` 📖	MathDef	5 math math: `nonnegg_comm`, `nonnegg_cases_left`, `nonnegg_cases_right`, `nonnegg_neg_pos`, `nonnegg_pos_neg`
`Nonsquare` 📖	CompData	1 math math: `Pell.dnsq`
`SqLe` 📖	MathDef	4 math math: `not_sqLe_succ`, `sqLe_mul`, `nonnegg_neg_pos`, `nonnegg_pos_neg`
`addCommGroup` 📖	CompOp	4 math math: `im_sub`, `re_sub`, `sub_im`, `sub_re`
`addGroupWithOne` 📖	CompOp	35 math math: `nonneg_smul`, `exists_coprime_of_gcd_pos`, `im_smul`, `intCast_im`, `re_intCast`, `le_arch`, `re_smul`, `natCast_im`, `GaussianInt.toComplex_sub`, `Pell.pellZd_succ_succ`, `ofInt_eq_intCast`, `smuld_val`, `nsmul_val`, `norm_eq_mul_conj`, `instCharZero`, `norm_intCast`, `intCast_dvd_intCast`, `intCast_val`, `mul_star`, `decompose`, `natCast_val`, `im_intCast`, `smul_val`, `GaussianInt.prime_of_nat_prime_of_mod_four_eq_three`, `norm_natCast`, `intCast_dvd`, `re_natCast`, `smul_im`, `dmuld`, `intCast_re`, `im_natCast`, `GaussianInt.mod_def`, `smul_re`, `GaussianInt.prime_iff_mod_four_eq_three_of_nat_prime`, `natCast_re`
`commRing` 📖	CompOp	6 math math: `Pell.is_pell_solution_iff_mem_unitary`, `mker_norm_eq_unitary`, `Pell.Solution₁.coe_mk`, `Pell.isPell_iff_mem_unitary`, `instIsOrderedAddMonoidCastInt`, `norm_eq_one_iff_mem_unitary`
`decidableLE` 📖	CompOp	—
`decidableNonneg` 📖	CompOp	—
`decidableNonnegg` 📖	CompOp	—
`im` 📖	CompOp	44 math math: `norm_def`, `ofInt_im`, `GaussianInt.natAbs_norm_eq`, `GaussianInt.intCast_im`, `im_sub`, `re_mul`, `im_ofNat`, `GaussianInt.toComplex_def₂`, `Pell.is_pell_solution_iff_mem_unitary`, `gcd_pos_iff`, `im_star`, `im_add`, `im_smul`, `intCast_im`, `mul_im`, `star_im`, `im_sqrtd`, `natCast_im`, `one_im`, `GaussianInt.toComplex_def`, `zero_im`, `GaussianInt.div_def`, `lift_apply_apply`, `GaussianInt.to_real_im`, `ofNat_im`, `add_im`, `im_zero`, `sub_im`, `im_one`, `im_intCast`, `intCast_dvd`, `Pell.im_pellZd`, `smul_im`, `im_mul`, `im_ofInt`, `toReal_apply`, `ext_iff`, `gcd_eq_zero_iff`, `im_natCast`, `sqrtd_im`, `Pell.pellZd_im`, `mul_re`, `im_neg`, `neg_im`
`instAdd` 📖	CompOp	12 math math: `im_add`, `add_re`, `GaussianInt.toComplex_add`, `Pell.pellZd_succ_succ`, `nonneg_add_lem`, `Nonneg.add`, `add_im`, `decompose`, `add_def`, `re_add`, `add_le_add_left`, `add_lt_add_left`
`instAddCommSemigroup` 📖	CompOp	—
`instAddMonoid` 📖	CompOp	—
`instAddSemigroup` 📖	CompOp	—
`instCommMonoid` 📖	CompOp	—
`instCommSemigroup` 📖	CompOp	—
`instCommSemiring` 📖	CompOp	2 math math: `GaussianInt.prime_of_nat_prime_of_mod_four_eq_three`, `GaussianInt.prime_iff_mod_four_eq_three_of_nat_prime`
`instDistrib` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instLECastInt` 📖	CompOp	5 math math: `le_arch`, `le_total`, `instZeroLEOneClassCastInt`, `nonneg_iff_zero_le`, `le_of_le_le`
`instLTCastInt` 📖	CompOp	—
`instMonoid` 📖	CompOp	8 math math: `Pell.is_pell_solution_iff_mem_unitary`, `norm_eq_one_iff`, `mker_norm_eq_unitary`, `Pell.Solution₁.coe_mk`, `norm_eq_one_iff'`, `Pell.isPell_iff_mem_unitary`, `isUnit_iff_norm_isUnit`, `norm_eq_one_iff_mem_unitary`
`instMul` 📖	CompOp	35 math math: `GaussianInt.toComplex_mul`, `nonneg_smul`, `re_mul`, `exists_coprime_of_gcd_pos`, `Pell.isPell_mul`, `Pell.pellZd_sub`, `muld_val`, `Pell.isPell_norm`, `instNoZeroDivisorsCastInt`, `Pell.pellZd_succ`, `GaussianInt.norm_le_norm_mul_left`, `im_smul`, `nonneg_mul_lem`, `mul_im`, `norm_mul`, `re_smul`, `mul_pos`, `Pell.pellZd_succ_succ`, `GaussianInt.div_def`, `smuld_val`, `nsmul_val`, `norm_eq_mul_conj`, `nonneg_mul`, `mul_star`, `decompose`, `smul_val`, `nonneg_muld`, `Pell.pellZd_add`, `smul_im`, `im_mul`, `dmuld`, `GaussianInt.mod_def`, `smul_re`, `mul_re`, `mul_nonneg`
`instNeg` 📖	CompOp	7 math math: `re_neg`, `nonneg_total`, `neg_re`, `norm_neg`, `GaussianInt.toComplex_neg`, `im_neg`, `neg_im`
`instOne` 📖	CompOp	8 math math: `norm_one`, `one_re`, `Pell.isPell_norm`, `one_im`, `instZeroLEOneClassCastInt`, `re_one`, `im_one`, `GaussianInt.toComplex_one`
`instRing` 📖	CompOp	—
`instSemigroup` 📖	CompOp	2 math math: `intCast_dvd_intCast`, `intCast_dvd`
`instSemiring` 📖	CompOp	37 math math: `GaussianInt.toComplex_mul`, `instIsDomainCastInt`, `GaussianInt.intCast_im`, `GaussianInt.toComplex_def'`, `instIsStrictOrderedRingCastInt`, `GaussianInt.toComplex_def₂`, `GaussianInt.toComplex_div_re`, `hom_ext_iff`, `GaussianInt.toComplex_injective`, `mker_norm_eq_unitary`, `GaussianInt.toComplex_im_div`, `lift_symm_apply_coe`, `GaussianInt.toComplex_add`, `GaussianInt.toComplex_sub`, `GaussianInt.toComplex_star`, `GaussianInt.toComplex_def`, `GaussianInt.to_real_re`, `lift_apply_apply`, `GaussianInt.to_real_im`, `GaussianInt.toComplex_re_div`, `GaussianInt.toComplex_re`, `GaussianInt.toComplex_inj`, `GaussianInt.intCast_real_norm`, `GaussianInt.toComplex_im`, `GaussianInt.im_toComplex`, `GaussianInt.toComplex_neg`, `GaussianInt.re_toComplex`, `GaussianInt.toComplex_zero`, `toReal_apply`, `lift_injective`, `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`, `toReal_injective`
`instStar` 📖	CompOp	13 math math: `Pell.pellZd_sub`, `im_star`, `Pell.isPell_norm`, `norm_conj`, `star_mk`, `star_im`, `GaussianInt.toComplex_star`, `GaussianInt.div_def`, `norm_eq_mul_conj`, `re_star`, `mul_star`, `Pell.isPell_star`, `star_re`
`instStarRing` 📖	CompOp	5 math math: `Pell.is_pell_solution_iff_mem_unitary`, `mker_norm_eq_unitary`, `Pell.Solution₁.coe_mk`, `Pell.isPell_iff_mem_unitary`, `norm_eq_one_iff_mem_unitary`
`instZero` 📖	CompOp	15 math math: `norm_eq_zero`, `GaussianInt.norm_eq_zero`, `re_zero`, `instNoZeroDivisorsCastInt`, `zero_im`, `instZeroLEOneClassCastInt`, `im_zero`, `nonneg_iff_zero_le`, `norm_zero`, `zero_re`, `GaussianInt.toComplex_zero`, `norm_eq_zero_iff`, `gcd_eq_zero_iff`, `nonneg_antisymm`, `GaussianInt.toComplex_eq_zero`
`linearOrder` 📖	CompOp	2 math math: `instIsStrictOrderedRingCastInt`, `instIsOrderedAddMonoidCastInt`
`norm` 📖	CompOp	30 math math: `norm_def`, `GaussianInt.natAbs_norm_eq`, `GaussianInt.norm_pos`, `norm_eq_zero`, `norm_one`, `abs_norm`, `GaussianInt.norm_eq_zero`, `GaussianInt.natCast_natAbs_norm`, `norm_eq_one_iff`, `GaussianInt.natAbs_norm_mod_lt`, `norm_eq_one_iff'`, `GaussianInt.norm_le_norm_mul_left`, `norm_conj`, `norm_mul`, `norm_eq_of_associated`, `GaussianInt.div_def`, `norm_eq_mul_conj`, `norm_intCast`, `norm_neg`, `GaussianInt.intCast_real_norm`, `GaussianInt.norm_mod_lt`, `norm_zero`, `norm_nonneg`, `norm_natCast`, `norm_eq_zero_iff`, `isUnit_iff_norm_isUnit`, `norm_eq_one_iff_mem_unitary`, `GaussianInt.norm_nonneg`, `GaussianInt.abs_natCast_norm`, `GaussianInt.intCast_complex_norm`
`normMonoidHom` 📖	CompOp	1 math math: `mker_norm_eq_unitary`
`ofInt` 📖	CompOp	5 math math: `ofInt_im`, `ofInt_re`, `re_ofInt`, `ofInt_eq_intCast`, `im_ofInt`
`preorder` 📖	CompOp	—
`re` 📖	CompOp	44 math math: `norm_def`, `GaussianInt.natAbs_norm_eq`, `re_mul`, `ofInt_re`, `GaussianInt.toComplex_def₂`, `one_re`, `Pell.is_pell_solution_iff_mem_unitary`, `gcd_pos_iff`, `re_zero`, `re_ofNat`, `re_ofInt`, `re_neg`, `re_sub`, `mul_im`, `re_intCast`, `re_smul`, `add_re`, `GaussianInt.toComplex_def`, `GaussianInt.to_real_re`, `Pell.re_pellZd`, `GaussianInt.div_def`, `lift_apply_apply`, `neg_re`, `re_star`, `sqrtd_re`, `Pell.pellZd_re`, `re_one`, `zero_re`, `intCast_dvd`, `star_re`, `re_natCast`, `re_add`, `im_mul`, `sub_re`, `toReal_apply`, `ext_iff`, `gcd_eq_zero_iff`, `intCast_re`, `smul_re`, `ofNat_re`, `mul_re`, `natCast_re`, `re_sqrtd`, `GaussianInt.intCast_re`
`sqrtd` 📖	CompOp	11 math math: `muld_val`, `hom_ext_iff`, `im_sqrtd`, `lift_symm_apply_coe`, `smuld_val`, `sqrtd_re`, `decompose`, `nonneg_muld`, `dmuld`, `sqrtd_im`, `re_sqrtd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_norm` 📖	mathematical	—	`abs` `instLatticeInt` `Int.instAddGroup` `norm`	—	`abs_of_nonneg` `Int.instAddLeftMono` `norm_nonneg`
`add_def` 📖	mathematical	—	`Zsqrtd` `instAdd`	—	—
`add_im` 📖	mathematical	—	`im` `Zsqrtd` `instAdd`	—	`im_add`
`add_le_add_left` 📖	mathematical	`Zsqrtd` `instLECastInt`	`instAdd`	—	`add_sub_add_right_eq_sub`
`add_lt_add_left` 📖	mathematical	`Zsqrtd` `instLTCastInt`	`instAdd`	—	`le_of_add_le_add_left`
`add_re` 📖	mathematical	—	`re` `Zsqrtd` `instAdd`	—	`re_add`
`d_pos` 📖	—	—	—	—	`lt_of_le_of_ne` `Nonsquare.ns`
`decompose` 📖	mathematical	—	`Zsqrtd` `instAdd` `AddGroupWithOne.toIntCast` `addGroupWithOne` `instMul` `sqrtd`	—	`ext` `re_intCast` `MulZeroClass.zero_mul` `mul_one` `im_intCast` `MulZeroClass.mul_zero` `add_zero` `one_mul` `zero_add`
`divides_sq_eq_zero` 📖	—	—	—	—	`mul_left_cancel₀` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `LT.lt.ne'` `mul_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `mul_comm` `mul_assoc` `mul_left_comm` `Nonsquare.ns` `dvd_mul_right`
`divides_sq_eq_zero_z` 📖	—	—	—	—	`divides_sq_eq_zero` `mul_assoc`
`dmuld` 📖	mathematical	—	`Zsqrtd` `instMul` `sqrtd` `AddGroupWithOne.toIntCast` `addGroupWithOne`	—	`ext` `MulZeroClass.mul_zero` `mul_one` `zero_add` `re_intCast` `add_zero` `im_intCast`
`eq_of_smul_eq_smul_left` 📖	—	`Zsqrtd` `instMul` `AddGroupWithOne.toIntCast` `addGroupWithOne`	—	—	`ext_iff` `re_smul` `mul_left_cancel₀` `IsCancelMulZero.toIsLeftCancelMulZero` `Int.instIsCancelMulZero` `im_smul`
`eq_zero_or_eq_zero_of_mul_eq_zero` 📖	—	`Zsqrtd` `instMul` `instZero`	—	—	`eq_neg_of_add_eq_zero_left` `divides_sq_eq_zero_z` `mul_right_cancel₀` `IsCancelMulZero.toIsRightCancelMulZero` `Int.instIsCancelMulZero` `mul_assoc` `mul_neg` `mul_left_comm` `neg_mul` `neg_neg`
`exists_coprime_of_gcd_pos` 📖	mathematical	`re` `im`	`Zsqrtd` `instMul` `AddGroupWithOne.toIntCast` `addGroupWithOne` `IsCoprime` `Int.instCommSemiring`	—	`Int.exists_gcd_one` `smul_val` `mul_comm` `Int.isCoprime_iff_gcd_eq_one`
`ext` 📖	—	`re` `im`	—	—	—
`ext_iff` 📖	mathematical	—	`re` `im`	—	`ext`
`gcd_eq_zero_iff` 📖	mathematical	—	`re` `im` `Zsqrtd` `instZero`	—	—
`gcd_pos_iff` 📖	mathematical	—	`re` `im`	—	`pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `gcd_eq_zero_iff`
`hom_ext` 📖	—	`DFunLike.coe` `RingHom` `Zsqrtd` `Semiring.toNonAssocSemiring` `instSemiring` `NonAssocRing.toNonAssocSemiring` `RingHom.instFunLike` `sqrtd`	—	—	`RingHom.ext` `decompose` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_intCast` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`
`hom_ext_iff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Zsqrtd` `Semiring.toNonAssocSemiring` `instSemiring` `NonAssocRing.toNonAssocSemiring` `RingHom.instFunLike` `sqrtd`	—	`hom_ext`
`im_add` 📖	mathematical	—	`im` `Zsqrtd` `instAdd`	—	—
`im_intCast` 📖	mathematical	—	`im` `Zsqrtd` `AddGroupWithOne.toIntCast` `addGroupWithOne`	—	—
`im_mul` 📖	mathematical	—	`im` `Zsqrtd` `instMul` `re`	—	—
`im_natCast` 📖	mathematical	—	`im` `Zsqrtd` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `addGroupWithOne`	—	—
`im_neg` 📖	mathematical	—	`im` `Zsqrtd` `instNeg`	—	—
`im_ofInt` 📖	mathematical	—	`im` `ofInt`	—	—
`im_ofNat` 📖	mathematical	—	`im`	—	—
`im_one` 📖	mathematical	—	`im` `Zsqrtd` `instOne`	—	—
`im_smul` 📖	mathematical	—	`im` `Zsqrtd` `instMul` `AddGroupWithOne.toIntCast` `addGroupWithOne`	—	`re_intCast` `im_intCast` `MulZeroClass.zero_mul` `add_zero`
`im_sqrtd` 📖	mathematical	—	`im` `sqrtd`	—	—
`im_star` 📖	mathematical	—	`im` `Star.star` `Zsqrtd` `instStar`	—	—
`im_sub` 📖	mathematical	—	`im` `Zsqrtd` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup`	—	—
`im_zero` 📖	mathematical	—	`im` `Zsqrtd` `instZero`	—	—
`instCharZero` 📖	mathematical	—	`CharZero` `Zsqrtd` `AddGroupWithOne.toAddMonoidWithOne` `addGroupWithOne`	—	`Int.instCharZero`
`instIsDomainCastInt` 📖	mathematical	—	`IsDomain` `Zsqrtd` `instSemiring`	—	`NoZeroDivisors.to_isDomain` `nontrivial` `instNoZeroDivisorsCastInt`
`instIsOrderedAddMonoidCastInt` 📖	mathematical	—	`IsOrderedAddMonoid` `Zsqrtd` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `linearOrder`	—	`add_le_add_left`
`instIsStrictOrderedRingCastInt` 📖	mathematical	—	`IsStrictOrderedRing` `Zsqrtd` `instSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `linearOrder`	—	`IsStrictOrderedRing.of_mul_pos` `instIsOrderedAddMonoidCastInt` `instZeroLEOneClassCastInt` `nontrivial` `mul_pos`
`instNoZeroDivisorsCastInt` 📖	mathematical	—	`NoZeroDivisors` `Zsqrtd` `instMul` `instZero`	—	`eq_zero_or_eq_zero_of_mul_eq_zero`
`instZeroLEOneClassCastInt` 📖	mathematical	—	`ZeroLEOneClass` `Zsqrtd` `instZero` `instOne` `instLECastInt`	—	—
`intCast_dvd` 📖	mathematical	—	`Zsqrtd` `semigroupDvd` `instSemigroup` `AddGroupWithOne.toIntCast` `addGroupWithOne` `re` `im`	—	`re_intCast` `im_intCast` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `add_zero` `smul_val` `ext_iff`
`intCast_dvd_intCast` 📖	mathematical	—	`Zsqrtd` `semigroupDvd` `instSemigroup` `AddGroupWithOne.toIntCast` `addGroupWithOne`	—	`intCast_dvd` `re_intCast` `im_intCast` `dvd_zero`
`intCast_im` 📖	mathematical	—	`im` `Zsqrtd` `AddGroupWithOne.toIntCast` `addGroupWithOne`	—	`im_intCast`
`intCast_re` 📖	mathematical	—	`re` `Zsqrtd` `AddGroupWithOne.toIntCast` `addGroupWithOne`	—	`re_intCast`
`intCast_val` 📖	mathematical	—	`Zsqrtd` `AddGroupWithOne.toIntCast` `addGroupWithOne`	—	`ext` `re_intCast` `im_intCast`
`isCoprime_of_dvd_isCoprime` 📖	—	`IsCoprime` `Int.instCommSemiring` `re` `im` `Zsqrtd` `semigroupDvd` `instSemigroup`	—	—	`isCoprime_of_dvd` `IsBezout.of_isPrincipalIdealRing` `EuclideanDomain.to_principal_ideal_domain` `zero_dvd_iff` `Int.instNontrivial` `ext` `intCast_dvd` `dvd_trans` `IsCoprime.isUnit_of_dvd'`
`isUnit_iff_norm_isUnit` 📖	mathematical	—	`IsUnit` `Zsqrtd` `instMonoid` `Int.instMonoid` `norm`	—	`Int.isUnit_iff_natAbs_eq` `norm_eq_one_iff`
`le_antisymm` 📖	—	`Zsqrtd` `instLECastInt`	—	—	`eq_of_sub_eq_zero` `nonneg_antisymm` `neg_sub`
`le_arch` 📖	mathematical	—	`Zsqrtd` `instLECastInt` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `addGroupWithOne`	—	`Nat.cast_zero` `zero_add` `Nat.cast_add` `Nat.cast_one` `neg_add_rev` `add_assoc` `add_neg_cancel_left` `add_neg_cancel` `LE.le.trans` `MulZeroClass.mul_zero` `add_zero` `sub_self` `mul_comm` `mul_left_comm` `mul_one` `add_sub_cancel_left`
`le_of_add_le_add_left` 📖	—	`Zsqrtd` `instLECastInt` `instAdd`	—	—	`add_neg_cancel_comm` `add_le_add_left`
`le_of_le_le` 📖	mathematical	—	`Zsqrtd` `instLECastInt`	—	—
`le_total` 📖	mathematical	—	`Zsqrtd` `instLECastInt`	—	`nonneg_total` `neg_sub`
`lift_apply_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Zsqrtd` `Semiring.toNonAssocSemiring` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Equiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `Distrib.toAdd` `re` `im`	—	—
`lift_injective` 📖	mathematical	—	`Zsqrtd` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Equiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift`	—	`injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Int.cast_injective` `norm_eq_mul_conj` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `MulZeroClass.zero_mul` `norm_eq_zero` `Int.cast_zero` `re_intCast` `im_intCast` `add_zero`
`lift_symm_apply_coe` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `DFunLike.coe` `Equiv` `RingHom` `Zsqrtd` `Semiring.toNonAssocSemiring` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `RingHom.instFunLike` `sqrtd`	—	—
`mker_norm_eq_unitary` 📖	mathematical	—	`MonoidHom.mker` `Zsqrtd` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `instSemiring` `Int.instSemiring` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `MonoidHom.instMonoidHomClass` `normMonoidHom` `unitary` `instMonoid` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `instStarRing`	—	`Submonoid.ext` `MonoidHom.instMonoidHomClass` `norm_eq_one_iff_mem_unitary`
`mul_im` 📖	mathematical	—	`im` `Zsqrtd` `instMul` `re`	—	`im_mul`
`mul_nonneg` 📖	mathematical	`Zsqrtd` `instLECastInt` `instZero`	`instMul`	—	`nonneg_mul`
`mul_pos` 📖	mathematical	`Zsqrtd` `instLTCastInt` `instZero`	`instMul`	—	`NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero` `instNoZeroDivisorsCastInt` `le_antisymm` `mul_nonneg` `le_of_lt` `ne_of_gt`
`mul_re` 📖	mathematical	—	`re` `Zsqrtd` `instMul` `im`	—	`re_mul`
`mul_star` 📖	mathematical	—	`Zsqrtd` `instMul` `Star.star` `instStar` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `addGroupWithOne` `AddGroupWithOne.toIntCast`	—	`ext` `mul_neg` `mul_comm` `sub_eq_add_neg` `re_intCast` `im_intCast` `MulZeroClass.mul_zero` `add_zero` `neg_add_cancel` `neg_zero`
`muld_val` 📖	mathematical	—	`Zsqrtd` `instMul` `sqrtd`	—	`ext` `MulZeroClass.zero_mul` `mul_one` `zero_add` `one_mul`
`natCast_im` 📖	mathematical	—	`im` `Zsqrtd` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `addGroupWithOne`	—	`im_natCast`
`natCast_re` 📖	mathematical	—	`re` `Zsqrtd` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `addGroupWithOne`	—	`re_natCast`
`natCast_val` 📖	mathematical	—	`Zsqrtd` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `addGroupWithOne`	—	—
`neg_im` 📖	mathematical	—	`im` `Zsqrtd` `instNeg`	—	`im_neg`
`neg_re` 📖	mathematical	—	`re` `Zsqrtd` `instNeg`	—	`re_neg`
`nonneg_add_lem` 📖	mathematical	`Nonneg`	`Zsqrtd` `instAdd`	—	`sqLe_cancel` `sqLe_of_le` `le_rfl` `one_mul` `not_le_of_gt` `nonnegg_pos_neg` `nonnegg_neg_pos` `add_def` `neg_add_eq_sub`
`nonneg_antisymm` 📖	mathematical	`Nonneg` `Zsqrtd` `instNeg`	`instZero`	—	`not_sqLe_succ` `d_pos` `le_antisymm` `one_mul` `not_divides_sq`
`nonneg_cases` 📖	—	`Nonneg`	—	—	—
`nonneg_iff_zero_le` 📖	mathematical	—	`Nonneg` `Zsqrtd` `instLECastInt` `instZero`	—	`sub_zero`
`nonneg_mul` 📖	mathematical	`Nonneg`	`Zsqrtd` `instMul`	—	`nonneg_cases` `nonneg_mul_lem` `mul_comm` `mul_neg` `neg_mul` `neg_neg` `add_comm` `neg_add_rev` `nonnegg_pos_neg` `sqLe_mul` `nonnegg_neg_pos`
`nonneg_mul_lem` 📖	mathematical	`Nonneg`	`Zsqrtd` `instMul`	—	`decompose` `right_distrib` `Distrib.rightDistribClass` `mul_assoc` `Int.cast_natCast` `Nonneg.add` `nonneg_smul` `nonneg_muld`
`nonneg_muld` 📖	mathematical	`Nonneg`	`Zsqrtd` `instMul` `sqrtd`	—	`nonneg_cases` `muld_val` `mul_neg` `nonnegg_neg_pos` `mul_comm` `mul_one` `mul_left_comm` `nonnegg_pos_neg`
`nonneg_smul` 📖	mathematical	`Nonneg`	`Zsqrtd` `instMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `addGroupWithOne`	—	`Int.cast_natCast` `nonneg_cases` `smul_val` `mul_neg` `Nat.cast_mul` `nonnegg_pos_neg` `sqLe_smul` `nonnegg_neg_pos`
`nonneg_total` 📖	mathematical	—	`Nonneg` `Zsqrtd` `instNeg`	—	—
`nonnegg_cases_left` 📖	mathematical	`SqLe`	`Nonnegg`	—	`nonnegg_comm` `nonnegg_cases_right`
`nonnegg_cases_right` 📖	mathematical	`SqLe`	`Nonnegg`	—	—
`nonnegg_comm` 📖	mathematical	—	`Nonnegg`	—	—
`nonnegg_neg_pos` 📖	mathematical	—	`Nonnegg` `SqLe`	—	`Nat.cast_zero` `neg_zero` `MulZeroClass.mul_zero` `Nat.instCanonicallyOrderedAdd`
`nonnegg_pos_neg` 📖	mathematical	—	`Nonnegg` `SqLe`	—	`nonnegg_comm` `nonnegg_neg_pos`
`nontrivial` 📖	mathematical	—	`Nontrivial` `Zsqrtd`	—	`Iff.not` `ext_iff`
`norm_conj` 📖	mathematical	—	`norm` `Star.star` `Zsqrtd` `instStar`	—	`instCharZero` `norm_eq_mul_conj` `star_star` `mul_comm`
`norm_def` 📖	mathematical	—	`norm` `re` `im`	—	—
`norm_eq_mul_conj` 📖	mathematical	—	`Zsqrtd` `AddGroupWithOne.toIntCast` `addGroupWithOne` `norm` `instMul` `Star.star` `instStar`	—	`ext` `mul_comm` `sub_eq_add_neg` `Int.cast_add` `Int.cast_mul` `Int.cast_neg` `re_intCast` `im_intCast` `MulZeroClass.mul_zero` `add_zero` `mul_neg` `neg_zero` `neg_add_cancel`
`norm_eq_of_associated` 📖	mathematical	`Associated` `Zsqrtd` `instMonoid`	`norm`	—	`norm_mul` `norm_eq_one_iff'` `Units.isUnit` `mul_one`
`norm_eq_one_iff` 📖	mathematical	—	`norm` `IsUnit` `Zsqrtd` `instMonoid`	—	`isUnit_iff_dvd_one` `le_total` `norm_eq_mul_conj` `instCharZero` `neg_mul_eq_mul_neg` `Int.cast_neg` `mul_eq_one` `Unique.instSubsingleton` `norm_one` `norm_mul`
`norm_eq_one_iff'` 📖	mathematical	—	`norm` `IsUnit` `Zsqrtd` `instMonoid`	—	`norm_eq_one_iff` `norm_nonneg`
`norm_eq_one_iff_mem_unitary` 📖	mathematical	—	`norm` `Zsqrtd` `Submonoid` `Monoid.toMulOneClass` `instMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `instStarRing`	—	`Unitary.mem_iff_self_mul_star` `norm_eq_mul_conj` `Nat.cast_one` `Int.cast_one` `instCharZero`
`norm_eq_zero` 📖	mathematical	—	`norm` `Zsqrtd` `instZero`	—	`ext_iff` `divides_sq_eq_zero_z` `Int.instCharZero` `sub_eq_zero` `le_antisymm` `mul_assoc` `mul_nonpos_of_nonpos_of_nonneg` `IsOrderedRing.toMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `LT.lt.le` `mul_self_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Int.instAddLeftMono` `eq_zero_of_mul_self_eq_zero` `IsStrictOrderedRing.noZeroDivisors` `MulZeroClass.mul_zero` `LT.lt.ne` `norm_zero`
`norm_eq_zero_iff` 📖	mathematical	—	`norm` `Zsqrtd` `instZero`	—	`mul_self_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `Int.instAddLeftMono` `neg_nonneg` `mul_nonpos_of_nonpos_of_nonneg` `IsOrderedRing.toMulPosMono` `LT.lt.le` `add_eq_zero_iff_of_nonneg` `covariant_swap_add_of_covariant_add` `mul_assoc` `sub_eq_add_neg` `norm_def` `ext` `eq_zero_of_mul_self_eq_zero` `IsStrictOrderedRing.noZeroDivisors` `mul_eq_zero` `neg_eq_zero` `LT.lt.ne` `norm_zero`
`norm_intCast` 📖	mathematical	—	`norm` `Zsqrtd` `AddGroupWithOne.toIntCast` `addGroupWithOne`	—	`re_intCast` `im_intCast` `MulZeroClass.mul_zero` `sub_zero`
`norm_mul` 📖	mathematical	—	`norm` `Zsqrtd` `instMul`	—	`Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.mul_one`
`norm_natCast` 📖	mathematical	—	`norm` `Zsqrtd` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `addGroupWithOne`	—	`norm_intCast`
`norm_neg` 📖	mathematical	—	`norm` `Zsqrtd` `instNeg`	—	`instCharZero` `norm_eq_mul_conj` `star_neg` `mul_neg` `neg_mul` `neg_neg`
`norm_nonneg` 📖	mathematical	—	`norm`	—	`add_nonneg` `Int.instAddLeftMono` `mul_self_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `mul_assoc` `neg_mul_eq_neg_mul` `mul_nonneg` `neg_nonneg`
`norm_one` 📖	mathematical	—	`norm` `Zsqrtd` `instOne`	—	`mul_one` `MulZeroClass.mul_zero` `sub_zero`
`norm_zero` 📖	mathematical	—	`norm` `Zsqrtd` `instZero`	—	`MulZeroClass.mul_zero` `sub_self`
`not_divides_sq` 📖	—	—	—	—	`divides_sq_eq_zero`
`not_sqLe_succ` 📖	mathematical	—	`SqLe`	—	`not_le_of_gt` `mul_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono`
`nsmul_val` 📖	mathematical	—	`Zsqrtd` `instMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `addGroupWithOne`	—	`ext` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `add_zero`
`ofInt_eq_intCast` 📖	mathematical	—	`ofInt` `Zsqrtd` `AddGroupWithOne.toIntCast` `addGroupWithOne`	—	`ext` `re_intCast` `im_intCast`
`ofInt_im` 📖	mathematical	—	`im` `ofInt`	—	`im_ofInt`
`ofInt_re` 📖	mathematical	—	`re` `ofInt`	—	`re_ofInt`
`ofNat_im` 📖	mathematical	—	`im`	—	`im_ofNat`
`ofNat_re` 📖	mathematical	—	`re`	—	`re_ofNat`
`one_im` 📖	mathematical	—	`im` `Zsqrtd` `instOne`	—	`im_one`
`one_re` 📖	mathematical	—	`re` `Zsqrtd` `instOne`	—	`re_one`
`re_add` 📖	mathematical	—	`re` `Zsqrtd` `instAdd`	—	—
`re_intCast` 📖	mathematical	—	`re` `Zsqrtd` `AddGroupWithOne.toIntCast` `addGroupWithOne`	—	—
`re_mul` 📖	mathematical	—	`re` `Zsqrtd` `instMul` `im`	—	—
`re_natCast` 📖	mathematical	—	`re` `Zsqrtd` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `addGroupWithOne`	—	—
`re_neg` 📖	mathematical	—	`re` `Zsqrtd` `instNeg`	—	—
`re_ofInt` 📖	mathematical	—	`re` `ofInt`	—	—
`re_ofNat` 📖	mathematical	—	`re`	—	—
`re_one` 📖	mathematical	—	`re` `Zsqrtd` `instOne`	—	—
`re_smul` 📖	mathematical	—	`re` `Zsqrtd` `instMul` `AddGroupWithOne.toIntCast` `addGroupWithOne`	—	`re_intCast` `im_intCast` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `add_zero`
`re_sqrtd` 📖	mathematical	—	`re` `sqrtd`	—	—
`re_star` 📖	mathematical	—	`re` `Star.star` `Zsqrtd` `instStar`	—	—
`re_sub` 📖	mathematical	—	`re` `Zsqrtd` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup`	—	—
`re_zero` 📖	mathematical	—	`re` `Zsqrtd` `instZero`	—	—
`smul_im` 📖	mathematical	—	`im` `Zsqrtd` `instMul` `AddGroupWithOne.toIntCast` `addGroupWithOne`	—	`im_smul`
`smul_re` 📖	mathematical	—	`re` `Zsqrtd` `instMul` `AddGroupWithOne.toIntCast` `addGroupWithOne`	—	`re_smul`
`smul_val` 📖	mathematical	—	`Zsqrtd` `instMul` `AddGroupWithOne.toIntCast` `addGroupWithOne`	—	`ext` `re_intCast` `im_intCast` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `add_zero`
`smuld_val` 📖	mathematical	—	`Zsqrtd` `instMul` `sqrtd` `AddGroupWithOne.toIntCast` `addGroupWithOne`	—	`ext` `re_intCast` `MulZeroClass.zero_mul` `mul_one` `im_intCast` `MulZeroClass.mul_zero` `add_zero` `one_mul` `zero_add`
`sqLe_add` 📖	—	`SqLe`	—	—	`sqLe_add_mixed` `mul_add` `Distrib.leftDistribClass` `mul_comm` `mul_left_comm` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `mul_assoc`
`sqLe_add_mixed` 📖	—	`SqLe`	—	—	`mul_left_comm` `mul_comm`
`sqLe_cancel` 📖	—	`SqLe`	—	—	`le_of_not_gt` `not_le_of_gt` `mul_add` `Distrib.leftDistribClass` `mul_comm` `mul_left_comm` `add_assoc` `sqLe_add_mixed` `le_of_lt` `lt_imp_lt_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `mul_assoc` `le_refl` `add_le_add_right` `add_le_add` `add_lt_add_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`sqLe_mul` 📖	mathematical	—	`SqLe`	—	`sub_nonneg_of_le` `covariant_swap_add_of_covariant_add` `Int.instAddLeftMono` `Int.ofNat_le_ofNat_of_le` `Int.le_of_ofNat_le_ofNat` `le_of_sub_nonneg` `one_mul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.mul_one`
`sqLe_of_le` 📖	—	`SqLe`	—	—	`mul_le_mul'` `Nat.instMulLeftMono` `covariant_swap_mul_of_covariant_mul` `mul_le_mul_right`
`sqLe_smul` 📖	—	`SqLe`	—	—	`mul_left_comm` `mul_assoc`
`sqrtd_im` 📖	mathematical	—	`im` `sqrtd`	—	`im_sqrtd`
`sqrtd_re` 📖	mathematical	—	`re` `sqrtd`	—	`re_sqrtd`
`star_im` 📖	mathematical	—	`im` `Star.star` `Zsqrtd` `instStar`	—	`im_star`
`star_mk` 📖	mathematical	—	`Star.star` `Zsqrtd` `instStar`	—	—
`star_re` 📖	mathematical	—	`re` `Star.star` `Zsqrtd` `instStar`	—	`re_star`
`sub_im` 📖	mathematical	—	`im` `Zsqrtd` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup`	—	`im_sub`
`sub_re` 📖	mathematical	—	`re` `Zsqrtd` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup`	—	`re_sub`
`zero_im` 📖	mathematical	—	`im` `Zsqrtd` `instZero`	—	`im_zero`
`zero_re` 📖	mathematical	—	`re` `Zsqrtd` `instZero`	—	`re_zero`

Zsqrtd.Nonneg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Zsqrtd.Nonneg`	`Zsqrtd` `Zsqrtd.instAdd`	—	`Zsqrtd.nonneg_cases` `Zsqrtd.nonnegg_cases_right` `Zsqrtd.sqLe_of_le` `le_of_neg_le_neg` `Int.instAddLeftMono` `covariant_swap_add_of_covariant_add` `add_comm` `Zsqrtd.nonnegg_pos_neg` `Zsqrtd.nonnegg_cases_left` `Zsqrtd.nonnegg_neg_pos` `Zsqrtd.sqLe_add` `Zsqrtd.add_def` `neg_add` `Nat.cast_add` `Zsqrtd.nonneg_add_lem`

Zsqrtd.Nonsquare

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ns` 📖	—	—	—	—	—
`ns'` 📖	—	—	—	—	`ns`

(root)

Definitions

Name	Category	Theorems
`Zsqrtd` 📖	CompData	105 math math: `Zsqrtd.instIsDomainCastInt`, `Zsqrtd.nonneg_smul`, `Zsqrtd.norm_eq_zero`, `Zsqrtd.im_sub`, `Zsqrtd.norm_one`, `Zsqrtd.re_mul`, `Zsqrtd.exists_coprime_of_gcd_pos`, `Pell.isPell_mul`, `Zsqrtd.instIsStrictOrderedRingCastInt`, `Zsqrtd.one_re`, `Pell.pellZd_sub`, `Pell.is_pell_solution_iff_mem_unitary`, `Zsqrtd.muld_val`, `Zsqrtd.hom_ext_iff`, `Zsqrtd.re_zero`, `Zsqrtd.im_star`, `Zsqrtd.norm_eq_one_iff`, `Zsqrtd.mker_norm_eq_unitary`, `Zsqrtd.im_add`, `Pell.isPell_norm`, `Pell.Solution₁.coe_mk`, `Zsqrtd.instNoZeroDivisorsCastInt`, `Pell.pellZd_succ`, `Zsqrtd.norm_eq_one_iff'`, `Zsqrtd.re_neg`, `Zsqrtd.norm_conj`, `Zsqrtd.re_sub`, `Zsqrtd.im_smul`, `Zsqrtd.nonneg_mul_lem`, `Zsqrtd.intCast_im`, `Zsqrtd.mul_im`, `Zsqrtd.star_mk`, `Zsqrtd.norm_mul`, `Zsqrtd.star_im`, `Zsqrtd.re_intCast`, `Zsqrtd.le_arch`, `Zsqrtd.lift_symm_apply_coe`, `Zsqrtd.re_smul`, `Zsqrtd.natCast_im`, `Zsqrtd.add_re`, `Pell.isPell_iff_mem_unitary`, `Zsqrtd.one_im`, `Zsqrtd.nonneg_total`, `Zsqrtd.zero_im`, `Pell.pellZd_succ_succ`, `Zsqrtd.ofInt_eq_intCast`, `Zsqrtd.smuld_val`, `Zsqrtd.le_total`, `Zsqrtd.nsmul_val`, `Zsqrtd.nonneg_add_lem`, `Zsqrtd.nontrivial`, `Zsqrtd.lift_apply_apply`, `Zsqrtd.norm_eq_mul_conj`, `Zsqrtd.nonneg_mul`, `Zsqrtd.instCharZero`, `Zsqrtd.neg_re`, `Zsqrtd.instZeroLEOneClassCastInt`, `Zsqrtd.Nonneg.add`, `Zsqrtd.norm_intCast`, `Zsqrtd.intCast_dvd_intCast`, `Zsqrtd.intCast_val`, `Zsqrtd.norm_neg`, `Zsqrtd.add_im`, `Zsqrtd.im_zero`, `Zsqrtd.re_star`, `Zsqrtd.sub_im`, `Zsqrtd.nonneg_iff_zero_le`, `Zsqrtd.mul_star`, `Zsqrtd.norm_zero`, `Pell.isPell_star`, `Zsqrtd.re_one`, `Zsqrtd.im_one`, `Zsqrtd.zero_re`, `Zsqrtd.decompose`, `Zsqrtd.add_def`, `Zsqrtd.natCast_val`, `Zsqrtd.instIsOrderedAddMonoidCastInt`, `Zsqrtd.im_intCast`, `Zsqrtd.smul_val`, `Zsqrtd.norm_natCast`, `Zsqrtd.nonneg_muld`, `Zsqrtd.intCast_dvd`, `Zsqrtd.star_re`, `Zsqrtd.norm_eq_zero_iff`, `Pell.pellZd_add`, `Zsqrtd.re_natCast`, `Zsqrtd.smul_im`, `Zsqrtd.isUnit_iff_norm_isUnit`, `Zsqrtd.re_add`, `Zsqrtd.im_mul`, `Zsqrtd.sub_re`, `Zsqrtd.toReal_apply`, `Zsqrtd.dmuld`, `Zsqrtd.lift_injective`, `Zsqrtd.norm_eq_one_iff_mem_unitary`, `Zsqrtd.gcd_eq_zero_iff`, `Zsqrtd.intCast_re`, `Zsqrtd.im_natCast`, `Zsqrtd.smul_re`, `Zsqrtd.le_of_le_le`, `Zsqrtd.mul_re`, `Zsqrtd.natCast_re`, `Zsqrtd.im_neg`, `Zsqrtd.neg_im`, `Zsqrtd.toReal_injective`
`instDecidableEqZsqrtd` 📖	CompOp	—
`«termℤ√_»` 📖	CompOp	—

instDecidableEqZsqrtd

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

---

← Back to Index