GaussSum

📁 Source: Mathlib/NumberTheory/DirichletCharacter/GaussSum.lean

Statistics

Metric	Count
Definitions	0
Theorems factorsThrough_of_gaussSum_ne_zero, gaussSum_aux_of_mulShift, gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive, gaussSum_mulShift_of_isPrimitive	4
Total	4

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factorsThrough_of_gaussSum_ne_zero 📖	mathematical	AddChar.mulShift ZMod CommRing.toRing ZMod.commRing CommRing.toCommMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AddChar AddMonoidWithOne.toAddMonoid CommMonoid.toMonoid AddChar.instOne	DirichletCharacter.FactorsThrough CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring	—	DirichletCharacter.factorsThrough_iff_ker_unitsMap MonoidHom.mem_ker MulChar.coe_toUnitHom IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero gaussSum_aux_of_mulShift
gaussSum_aux_of_mulShift 📖	mathematical	AddChar.mulShift ZMod CommRing.toRing ZMod.commRing CommRing.toCommMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AddChar AddMonoidWithOne.toAddMonoid CommMonoid.toMonoid AddChar.instOne DFunLike.coe MonoidHom Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike ZMod.unitsMap Units.instOne	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DirichletCharacter CommSemiring.toCommMonoidWithZero MulChar.instFunLike Units.val gaussSum ZMod.fintype	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add 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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add AddChar.mulShift_mul AddChar.mulShift_one mul_eq_right RightCancelSemigroup.toIsRightCancelMul ZMod.charP ZMod.natCast_val ZMod.intCast_cast ZMod.intCast_eq_intCast_iff_dvd_sub Int.cast_one MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MonoidHom.coe_coe Units.coe_map ZMod.unitsMap_def Units.val_one Int.cast_sub ZMod.cast_id' AddChar.ext Int.cast_mul Int.cast_natCast mul_assoc DFunLike.ext_iff gaussSum_mulShift
gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive 📖	mathematical	DirichletCharacter.IsPrimitive CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring AddChar.IsPrimitive ZMod ZMod.commRing CommRing.toCommMonoid	gaussSum ZMod.fintype MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Mathlib.Tactic.Contrapose.contrapose₁ AddChar.exists_divisor_of_not_isPrimitive Nat.sInf_le factorsThrough_of_gaussSum_ne_zero LT.lt.ne LE.le.trans_lt
gaussSum_mulShift_of_isPrimitive 📖	mathematical	DirichletCharacter.IsPrimitive CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring	gaussSum ZMod ZMod.commRing ZMod.fintype AddChar.mulShift CommRing.toRing CommRing.toCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe DirichletCharacter MulChar.instFunLike MulChar.hasInv	—	gaussSum_mulShift IsUnit.unit_spec MulChar.inv_apply_eq_inv Ring.inverse_mul_cancel_left IsUnit.map MulCharClass.toMonoidHomClass MulChar.instMulCharClass MulChar.map_nonunit MulZeroClass.zero_mul gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive AddChar.not_isPrimitive_mulShift Finite.of_fintype

---

← Back to Index