Documentation Verification Report

GaussSum

📁 Source: Mathlib/NumberTheory/GaussSum.lean

Statistics

Metric	Count
Definitions `gaussSum`	1
Theorems `card_pow_card`, `card_pow_char_pow`, `two_pow_card`, `gaussSum_frob`, `gaussSum_frob_iter`, `gaussSum_frob`, `gaussSum_mul`, `gaussSum_mulShift`, `gaussSum_mul_gaussSum_eq_card`, `gaussSum_mul_gaussSum_pow_orderOf_sub_one`, `gaussSum_ne_zero_of_nontrivial`, `gaussSum_sq`, `mul_gaussSum_inv_eq_gaussSum`	13
Total	14

Char

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_pow_card` 📖	mathematical	`MulChar.IsQuadratic` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `MulChar` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `MulChar.instFunLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toNatCast` `Fintype.card`	—	`FiniteField.card` `ringChar.charP` `Finite.of_fintype` `Algebra.ringChar_eq` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `RingHom.injective` `DivisionRing.isSimpleRing` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_natCast` `Nat.cast_pow` `card_pow_char_pow` `instIsDomain` `MulChar.IsQuadratic.comp` `isUnit_iff_not_dvd_char` `Nat.prime_dvd_prime_iff_eq` `gaussSum_sq` `MulChar.ringHomComp_ne_one_iff` `AddChar.PrimitiveAddChar.prim`
`card_pow_char_pow` 📖	mathematical	`MulChar.IsQuadratic` `CommRing.toCommMonoid` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Monoid.toNatPow` `gaussSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `MulChar` `CommSemiring.toCommMonoidWithZero` `MulChar.instFunLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `Fintype.card`	`Nat.instMonoid`	—	`not_isUnit_prime_of_dvd_card` `CharP.cast_eq_zero_iff` `mul_eq_zero` `IsDomain.to_noZeroDivisors` `zero_pow` `two_ne_zero` `IsUnit.ne_zero` `IsDomain.toNontrivial` `IsUnit.map` `MulCharClass.toMonoidHomClass` `MulChar.instMulCharClass` `IsUnit.neg` `isUnit_one` `mul_right_cancel₀` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `MulChar.IsQuadratic.gaussSum_frob_iter` `pow_mul` `pow_succ` `Nat.two_mul_div_two_add_one_of_odd` `Odd.pow` `Nat.Prime.eq_two_or_odd'` `Fact.out`

FiniteField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`two_pow_card` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Nat.instAtLeastTwoHAddOfNat` `Fintype.card` `AddGroupWithOne.toIntCast` `DFunLike.coe` `MulChar` `ZMod` `CommRing.toCommMonoid` `ZMod.commRing` `CommSemiring.toCommMonoidWithZero` `Int.instCommSemiring` `MulChar.instFunLike` `ZMod.χ₈` `CommRing.toRing`	—	`Nat.instAtLeastTwoHAddOfNat` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `Ring.two_ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `card` `ringChar.charP` `Algebra.ringChar_eq` `isUnit_iff_not_dvd_char` `Finite.of_fintype` `ZMod.ringChar_zmod_n` `Nat.Prime.dvd_of_dvd_pow` `Nat.prime_dvd_prime_iff_eq` `Nat.prime_two` `sq_eq_one_iff` `pow_mul` `AddChar.map_nsmul_eq_pow` `AddChar.IsPrimitive.zmod_char_eq_one_iff` `NeZero.pnat` `AddChar.PrimitiveAddChar.prim` `Int.cast_one` `MulChar.IsQuadratic.comp` `ZMod.isQuadratic_χ₈` `pow_one` `gaussSum.eq_1` `Fin.sum_univ_eight` `Int.cast_zero` `MulZeroClass.zero_mul` `one_mul` `zero_add` `add_zero` `Int.cast_neg` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.LinearCombination.mul_const_eq` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `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.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `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.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `ZMod.card` `Nat.cast_ofNat` `Mathlib.Tactic.Ring.pow_nat` `Mathlib.Tactic.Ring.coeff_one` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_bit0` `Mathlib.Tactic.Ring.pow_one` `Mathlib.Meta.NormNum.isNat_mul` `Char.card_pow_char_pow` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `mul_pow` `isSquare_iff` `pow_two` `RingHom.injective` `DivisionRing.isSimpleRing` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_ofNat` `map_intCast` `Nat.cast_pow`

MulChar.IsQuadratic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gaussSum_frob` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `MulChar.IsQuadratic` `CommRing.toCommMonoid`	`Monoid.toNatPow` `gaussSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `MulChar` `CommSemiring.toCommMonoidWithZero` `MulChar.instFunLike`	—	`gaussSum_frob` `AddChar.pow_mulShift` `pow_char` `gaussSum_mulShift` `mul_assoc` `IsUnit.unit_spec` `pow_two` `MulChar.pow_apply'` `two_ne_zero` `sq_eq_one` `MulChar.one_apply_coe` `one_mul`
`gaussSum_frob_iter` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `MulChar.IsQuadratic` `CommRing.toCommMonoid`	`Monoid.toNatPow` `gaussSum` `Nat.instMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `MulChar` `CommSemiring.toCommMonoidWithZero` `MulChar.instFunLike`	—	`pow_zero` `pow_one` `MulChar.map_one` `one_mul` `pow_succ` `pow_mul` `mul_pow` `gaussSum_frob` `mul_assoc` `map_mul` `MonoidHomClass.toMulHomClass` `MulCharClass.toMonoidHomClass` `MulChar.instMulCharClass` `MulChar.pow_apply'` `Nat.Prime.ne_zero` `Fact.out` `pow_char`

(root)

Definitions

Name	Category	Theorems
`gaussSum` 📖	CompOp	18 math math: `jacobiSum_mul_nontrivial`, `gaussSum_mul`, `gaussSum_frob`, `mul_gaussSum_inv_eq_gaussSum`, `gaussSum_aux_of_mulShift`, `gaussSum_mulShift_of_isPrimitive`, `MulChar.IsQuadratic.gaussSum_frob_iter`, `jacobiSum_eq_gaussSum_mul_gaussSum_div_gaussSum`, `DirichletCharacter.IsPrimitive.fourierTransform_eq_inv_mul_gaussSum`, `gaussSum_pow_eq_prod_jacobiSum_aux`, `gaussSum_mul_gaussSum_pow_orderOf_sub_one`, `MulChar.IsQuadratic.gaussSum_frob`, `gaussSum_pow_eq_prod_jacobiSum`, `gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive`, `DirichletCharacter.fourierTransform_eq_gaussSum_mulShift`, `gaussSum_mul_gaussSum_eq_card`, `gaussSum_sq`, `gaussSum_mulShift`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gaussSum_frob` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `gaussSum` `MulChar` `CommRing.toCommMonoid` `CommSemiring.toCommMonoidWithZero` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MulChar.commGroup` `AddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddChar.instCommGroup` `Ring.toAddCommGroup`	—	`expChar_prime` `frobenius_def` `gaussSum.eq_1` `map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Finset.sum_congr` `MulChar.pow_apply'` `Nat.Prime.ne_zero` `Fact.out` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`
`gaussSum_mul` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `gaussSum` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.univ` `DFunLike.coe` `MulChar` `CommRing.toCommMonoid` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `MulChar.instFunLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `AddChar.instFunLike`	—	`gaussSum.eq_1` `Finset.sum_mul_sum` `mul_mul_mul_comm` `Finset.sum_congr` `AddChar.map_add_eq_mul` `Finset.sum_bij` `AddTorsor.nonempty` `AddRightCancelSemigroup.toIsRightCancelAdd` `Finset.mem_univ` `sub_add_cancel` `add_sub_cancel_right` `add_comm` `Finset.sum_comm`
`gaussSum_mulShift` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `MulChar` `CommRing.toCommMonoid` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `MulChar.instFunLike` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `gaussSum` `AddChar.mulShift` `CommRing.toRing`	—	`Finset.sum_congr` `Finset.mul_sum` `MonoidHomClass.toMulHomClass` `MulCharClass.toMonoidHomClass` `MulChar.instMulCharClass` `Fintype.sum_bijective` `Units.mulLeft_bijective`
`gaussSum_mul_gaussSum_eq_card` 📖	mathematical	`AddChar.IsPrimitive` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toCommMonoid`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `gaussSum` `MulChar` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `MulChar.hasInv` `AddChar` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `AddChar.instCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toNatCast` `Fintype.card`	—	`Finset.sum_congr` `MulChar.inv_apply'` `Finset.mul_sum` `Finset.sum_mul` `mul_mul_mul_comm` `map_mul` `MonoidHomClass.toMulHomClass` `MulCharClass.toMonoidHomClass` `MulChar.instMulCharClass` `AddChar.map_add_eq_mul` `sub_eq_add_neg` `Finset.sum_comm` `AddChar.sum_mulShift` `Nat.cast_zero` `MulZeroClass.mul_zero` `Finset.sum_ite_eq'` `map_one` `MonoidHomClass.toOneHomClass` `one_mul`
`gaussSum_mul_gaussSum_pow_orderOf_sub_one` 📖	mathematical	`AddChar.IsPrimitive` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toCommMonoid`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `gaussSum` `MulChar` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MulChar.commGroup` `orderOf` `DFunLike.coe` `MulChar.instFunLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toNatCast` `CommRing.toRing` `Fintype.card`	—	`inv_eq_of_mul_eq_one_right` `pow_succ'` `MulChar.orderOf_pos` `instFiniteUnits` `Finite.of_fintype` `pow_orderOf_eq_one` `mul_gaussSum_inv_eq_gaussSum` `mul_left_comm` `gaussSum_mul_gaussSum_eq_card` `MulChar.inv_apply'` `inv_neg_one`
`gaussSum_ne_zero_of_nontrivial` 📖	—	`AddChar.IsPrimitive` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toCommMonoid`	—	—	`gaussSum_mul_gaussSum_eq_card` `MulZeroClass.zero_mul`
`gaussSum_sq` 📖	mathematical	`MulChar.IsQuadratic` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddChar.IsPrimitive`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `gaussSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `MulChar` `CommSemiring.toCommMonoidWithZero` `MulChar.instFunLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toNatCast` `CommRing.toRing` `Fintype.card`	—	`pow_two` `gaussSum_mul_gaussSum_eq_card` `MulChar.IsQuadratic.inv` `mul_rotate'` `mul_comm` `gaussSum_mulShift` `AddChar.inv_mulShift`
`mul_gaussSum_inv_eq_gaussSum` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `MulChar` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `MulChar.instFunLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `gaussSum` `AddChar` `AddMonoidWithOne.toAddMonoid` `CommRing.toRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `AddChar.instCommGroup`	—	`AddChar.inv_mulShift` `Units.coe_neg_one` `gaussSum_mulShift`

---

← Back to Index