Documentation Verification Report

Complex

📁 Source: Mathlib/RingTheory/RootsOfUnity/Complex.lean

Statistics

Metric	Count
Definitions	0
Theorems `card_primitiveRoots`, `card_rootsOfUnity`, `conj_rootsOfUnity`, `isPrimitiveRoot_exp`, `isPrimitiveRoot_exp_of_coprime`, `isPrimitiveRoot_exp_of_isCoprime`, `isPrimitiveRoot_exp_rat`, `isPrimitiveRoot_exp_rat_of_even_num`, `isPrimitiveRoot_exp_rat_of_odd_num`, `isPrimitiveRoot_iff`, `mem_rootsOfUnity`, `norm_eq_one_of_mem_rootsOfUnity`, `arg`, `arg_eq_pi_iff`, `arg_eq_zero_iff`, `arg_ext`, `nnnorm_eq_one`, `norm'_eq_one`	18
Total	18

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_primitiveRoots` 📖	mathematical	—	`Finset.card` `Complex` `primitiveRoots` `commRing` `instIsDomain` `Field.toSemifield` `instField` `Nat.totient`	—	`instIsDomain` `primitiveRoots.congr_simp` `primitiveRoots_zero` `IsPrimitiveRoot.card_primitiveRoots` `Nat.instAtLeastTwoHAddOfNat` `isPrimitiveRoot_exp`
`card_rootsOfUnity` 📖	mathematical	—	`Fintype.card` `Units` `Complex` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `commRing` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `rootsOfUnity.fintype` `instIsDomain` `Field.toSemifield` `instField`	—	`IsPrimitiveRoot.card_rootsOfUnity` `instIsDomain` `Nat.instAtLeastTwoHAddOfNat` `isPrimitiveRoot_exp`
`conj_rootsOfUnity` 📖	mathematical	`Units` `Complex` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Subgroup` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `commRing` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.instFunLike` `starRingEnd` `instStarRing` `Units.val` `Units.instInv`	—	`Units.mul_eq_one_iff_eq_inv` `conj_mul'` `norm_eq_one_of_mem_rootsOfUnity` `ofReal_one` `one_pow`
`isPrimitiveRoot_exp` 📖	mathematical	—	`IsPrimitiveRoot` `Complex` `CommRing.toCommMonoid` `commRing` `exp` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I`	—	`Nat.instAtLeastTwoHAddOfNat` `Nat.cast_one` `one_div` `isPrimitiveRoot_exp_of_coprime`
`isPrimitiveRoot_exp_of_coprime` 📖	mathematical	—	`IsPrimitiveRoot` `Complex` `CommRing.toCommMonoid` `commRing` `exp` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`isPrimitiveRoot_exp_of_isCoprime` `Nat.Coprime.isCoprime`
`isPrimitiveRoot_exp_of_isCoprime` 📖	mathematical	`IsCoprime` `Int.instCommSemiring`	`IsPrimitiveRoot` `Complex` `CommRing.toCommMonoid` `commRing` `exp` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I` `DivInvMonoid.toDiv` `instDivInvMonoid` `instIntCast`	—	`Nat.instAtLeastTwoHAddOfNat` `IsPrimitiveRoot.iff_def` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `one_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.cons_zero_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Mathlib.Meta.NormNum.isNat_eq_false` `instCharZero` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `mul_div_cancel_left₀` `EuclideanDomain.toMulDivCancelClass` `IsCoprime.dvd_of_dvd_mul_right` `IsCoprime.symm` `dvd_mul_right` `Int.cast_natCast` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg`
`isPrimitiveRoot_exp_rat` 📖	mathematical	—	`IsPrimitiveRoot` `Complex` `CommRing.toCommMonoid` `commRing` `exp` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I` `instRatCast`	—	`Nat.instAtLeastTwoHAddOfNat` `Rat.num_div_den` `Rat.cast_div` `instCharZero` `Rat.cast_intCast` `Rat.cast_natCast` `isPrimitiveRoot_exp_of_isCoprime` `Int.isCoprime_iff_nat_coprime`
`isPrimitiveRoot_exp_rat_of_even_num` 📖	mathematical	`Even`	`IsPrimitiveRoot` `Complex` `CommRing.toCommMonoid` `commRing` `exp` `instMul` `ofReal` `Real.pi` `I` `instRatCast`	—	`even_iff_exists_two_nsmul` `Nat.instAtLeastTwoHAddOfNat` `Rat.num_div_den` `Int.nsmul_eq_mul` `Int.cast_mul` `Int.cast_ofNat` `Rat.cast_div` `instCharZero` `Rat.cast_mul` `Rat.cast_ofNat` `Rat.cast_intCast` `Rat.cast_natCast` `Mathlib.Tactic.Ring.mul_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.div_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero` `Int.cast_natCast` `isPrimitiveRoot_exp_rat`
`isPrimitiveRoot_exp_rat_of_odd_num` 📖	mathematical	`Odd` `Int.instSemiring`	`IsPrimitiveRoot` `Complex` `CommRing.toCommMonoid` `commRing` `exp` `instMul` `ofReal` `Real.pi` `I` `instRatCast`	—	`Nat.instAtLeastTwoHAddOfNat` `Rat.cast_div` `instCharZero` `Rat.cast_ofNat` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero` `Rat.num_div_den` `mul_comm` `div_div` `Int.cast_ofNat` `Int.cast_natCast` `Int.cast_mul` `Nat.cast_ofNat` `Nat.cast_mul` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `Nat.instCharZero` `Odd.coprime_two_right` `Odd.natAbs` `isPrimitiveRoot_exp_rat`
`isPrimitiveRoot_iff` 📖	mathematical	—	`IsPrimitiveRoot` `Complex` `CommRing.toCommMonoid` `commRing` `exp` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`Nat.cast_zero` `instCharZero` `Nat.instAtLeastTwoHAddOfNat` `IsPrimitiveRoot.eq_pow_of_pow_eq_one` `instIsDomain` `isPrimitiveRoot_exp` `IsPrimitiveRoot.pow_eq_one` `IsPrimitiveRoot.pow_iff_coprime` `exp_nat_mul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.one_mul` `isPrimitiveRoot_exp_of_coprime`
`mem_rootsOfUnity` 📖	mathematical	—	`Units` `Complex` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Subgroup` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `commRing` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `exp` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I` `DivInvMonoid.toDiv` `instDivInvMonoid` `Units.val`	—	`Nat.instAtLeastTwoHAddOfNat` `mem_rootsOfUnity` `Units.ext_iff` `Units.val_pow_eq_pow_val` `Units.val_one` `Nat.cast_zero` `instCharZero` `IsPrimitiveRoot.eq_pow_of_pow_eq_one` `instIsDomain` `isPrimitiveRoot_exp` `exp_nat_mul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.one_mul` `exp_eq_one_iff` `Int.cast_natCast` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `one_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Mathlib.Meta.NormNum.isNat_eq_false` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial`
`norm_eq_one_of_mem_rootsOfUnity` 📖	mathematical	`Units` `Complex` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Subgroup` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `commRing` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity`	`Norm.norm` `instNorm` `Units.val` `Real` `Real.instOne`	—	`norm_eq_one_of_pow_eq_one` `Nat.cast_one` `mem_rootsOfUnity` `Units.val_one`

IsPrimitiveRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arg` 📖	mathematical	`IsPrimitiveRoot` `Complex` `CommRing.toCommMonoid` `Complex.commRing`	`Complex.arg` `Real` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instIntCast` `Real.instNatCast` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `IsCoprime` `Int.instCommSemiring`	—	`Nat.instAtLeastTwoHAddOfNat` `Complex.isPrimitiveRoot_iff` `mul_comm` `mul_assoc` `Complex.exp_mul_I` `Int.cast_natCast` `Complex.ofReal_mul` `Complex.ofReal_div` `Complex.arg_cos_add_sin_mul_I` `LT.lt.trans_le` `neg_lt_neg` `Real.instIsOrderedAddMonoid` `Real.pi_pos` `neg_zero` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instZeroLEOneClass` `Nat.cast_pos'` `NeZero.charZero_one` `RCLike.charZero_rclike` `lt_of_le_of_ne'` `zero_le` `Nat.instCanonicallyOrderedAdd` `le_of_lt` `mul_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Eq.trans_le` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.mul_one` `mul_le_of_le_one_right` `LT.lt.le` `div_le_iff₀'` `Nat.cast_zero` `pos_of_gt` `Nat.cast_one` `mul_one` `Complex.cos_sub_two_pi` `Complex.sin_sub_two_pi` `Int.cast_sub` `Complex.ofReal_sub` `sub_one_mul` `sub_div` `div_self` `Complex.instCharZero` `Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `LT.lt.ne'` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `mul_neg` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.cons_pos` `zero_lt_one` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.FieldSimp.le_eq_cancel_le` `PosMulStrictMono.toPosMulMono` `Mathlib.Tactic.LinearCombination.lt_of_lt` `Real.instIsOrderedCancelAddMonoid` `Nat.cast_mul` `Int.cast_mul` `Int.cast_ofNat` `Rat.cast_natCast` `Rat.cast_mul` `Mathlib.Tactic.LinearCombination.le_rearrange` `Mathlib.Tactic.Ring.le_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `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_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `le_refl` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.LinearCombination.le_of_lt` `add_lt_add` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `Mathlib.Tactic.LinearCombination.mul_const_lt` `one_pos` `Mathlib.Meta.NormNum.isNat_add` `Nat.isCoprime_iff_coprime` `mul_neg_one` `sub_eq_add_neg` `IsCoprime.add_mul_left_left`
`arg_eq_pi_iff` 📖	mathematical	`IsPrimitiveRoot` `Complex` `CommRing.toCommMonoid` `Complex.commRing`	`Complex.arg` `Real.pi` `Complex.instNeg` `Complex.instOne`	—	`arg_ext` `neg_one` `Complex.instNontrivial` `CharP.ofCharZero` `Complex.instCharZero` `two_ne_zero` `Complex.arg_neg_one`
`arg_eq_zero_iff` 📖	mathematical	`IsPrimitiveRoot` `Complex` `CommRing.toCommMonoid` `Complex.commRing`	`Complex.arg` `Real` `Real.instZero` `Complex.instOne`	—	`arg_ext` `one` `one_ne_zero` `Complex.arg_one`
`arg_ext` 📖	—	`IsPrimitiveRoot` `Complex` `CommRing.toCommMonoid` `Complex.commRing` `Complex.arg`	—	—	`Complex.ext_norm_arg` `norm'_eq_one`
`nnnorm_eq_one` 📖	mathematical	`IsPrimitiveRoot` `Complex` `CommRing.toCommMonoid` `Complex.commRing`	`NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NNReal` `instOneNNReal`	—	`norm'_eq_one`
`norm'_eq_one` 📖	mathematical	`IsPrimitiveRoot` `Complex` `CommRing.toCommMonoid` `Complex.commRing`	`Norm.norm` `Complex.instNorm` `Real` `Real.instOne`	—	`Complex.norm_eq_one_of_pow_eq_one` `pow_eq_one`

---

← Back to Index