Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `jacobiSum`	1
Theorems `exists_jacobiSum_eq_neg_one_add`, `gaussSum_pow_eq_prod_jacobiSum`, `gaussSum_pow_eq_prod_jacobiSum_aux`, `jacobiSum_comm`, `jacobiSum_eq_gaussSum_mul_gaussSum_div_gaussSum`, `jacobiSum_eq_sum_sdiff`, `jacobiSum_mem_algebraAdjoin_of_pow_eq_one`, `jacobiSum_mul_jacobiSum_inv`, `jacobiSum_mul_nontrivial`, `jacobiSum_nontrivial_inv`, `jacobiSum_one_nontrivial`, `jacobiSum_one_one`, `jacobiSum_ringHomComp`, `jacobiSum_trivial_trivial`	14
Total	15

(root)

Definitions

Name	Category	Theorems
`jacobiSum` 📖	CompOp	14 math math: `jacobiSum_mem_algebraAdjoin_of_pow_eq_one`, `jacobiSum_mul_nontrivial`, `jacobiSum_trivial_trivial`, `jacobiSum_one_nontrivial`, `exists_jacobiSum_eq_neg_one_add`, `jacobiSum_eq_gaussSum_mul_gaussSum_div_gaussSum`, `gaussSum_pow_eq_prod_jacobiSum_aux`, `jacobiSum_nontrivial_inv`, `jacobiSum_comm`, `gaussSum_pow_eq_prod_jacobiSum`, `jacobiSum_eq_sum_sdiff`, `jacobiSum_mul_jacobiSum_inv`, `jacobiSum_ringHomComp`, `jacobiSum_one_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_jacobiSum_eq_neg_one_add` 📖	mathematical	`MulChar` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MulChar.commGroup` `MulChar.hasOne` `Fintype.card` `IsPrimitiveRoot`	`Subalgebra` `Int.instCommSemiring` `CommSemiring.toSemiring` `Ring.toIntAlgebra` `CommRing.toRing` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `jacobiSum` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Distrib.toMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	—	`IsPrimitiveRoot.self_sub_one_pow_dvd_order` `Nat.instAtLeastTwoHAddOfNat` `jacobiSum_one_one` `Subalgebra.mul_mem` `Subalgebra.natCast_mem` `NeZero.one_le` `Fintype.instNeZeroNatCardOfNonempty` `Nontrivial.to_nonempty` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Nat.cast_add` `Nat.cast_mul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_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.pow_add` `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.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.neg_congr` `Subalgebra.zero_mem` `jacobiSum_one_nontrivial` `MulZeroClass.zero_mul` `add_zero` `jacobiSum_comm` `MulChar.sum_eq_zero_of_ne_one` `Finite.of_fintype` `Subalgebra.add_mem` `Subalgebra.neg_mem` `Subalgebra.sum_mem` `Finset.sum_mul` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.neg_mul`
`gaussSum_pow_eq_prod_jacobiSum` 📖	mathematical	`orderOf` `MulChar` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MulChar.commGroup` `AddChar.IsPrimitive`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `gaussSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `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` `Finset.prod` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `jacobiSum`	—	`gaussSum_pow_eq_prod_jacobiSum_aux` `LT.lt.false` `LE.le.trans_lt` `orderOf_one` `pow_succ'` `mul_assoc` `gaussSum_mul_gaussSum_pow_orderOf_sub_one`
`gaussSum_pow_eq_prod_jacobiSum_aux` 📖	mathematical	`orderOf` `MulChar` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MulChar.commGroup`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `gaussSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.prod` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `jacobiSum`	—	`Nat.le_induction` `pow_one` `Finset.prod_congr` `Finset.Ico_eq_empty_of_le` `mul_one` `pow_ne_one_of_lt_orderOf` `pow_succ'` `mul_comm` `jacobiSum_mul_nontrivial` `pow_succ` `mul_right_comm` `lt_trans` `Finset.prod_Ico_succ_top` `mul_rotate` `mul_assoc`
`jacobiSum_comm` 📖	mathematical	—	`jacobiSum`	—	`Finset.sum_congr` `mul_comm` `Equiv.sum_comp` `sub_sub_cancel`
`jacobiSum_eq_gaussSum_mul_gaussSum_div_gaussSum` 📖	mathematical	`AddChar.IsPrimitive` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toCommMonoid`	`jacobiSum` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `gaussSum` `MulChar` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `MulChar.hasMul`	—	`eq_div_iff` `gaussSum_ne_zero_of_nontrivial` `instIsDomain` `mul_comm` `jacobiSum_mul_nontrivial`
`jacobiSum_eq_sum_sdiff` 📖	mathematical	—	`jacobiSum` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset` `Finset.instSDiff` `Finset.univ` `Finset.instInsert` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Finset.instSingleton` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `MulChar` `CommRing.toCommMonoid` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `MulChar.instFunLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	—	`Finset.sum_congr` `sub_eq_add_neg` `Finset.sum_sdiff_eq_sub` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Finset.sum_eq_zero` `MulChar.map_zero` `neg_zero` `add_zero` `map_one` `MonoidHomClass.toOneHomClass` `MulCharClass.toMonoidHomClass` `MulChar.instMulCharClass` `mul_one` `add_neg_cancel` `MulZeroClass.mul_zero`
`jacobiSum_mem_algebraAdjoin_of_pow_eq_one` 📖	mathematical	`MulChar` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MulChar.commGroup` `MulChar.hasOne` `IsPrimitiveRoot`	`Subalgebra` `Int.instCommSemiring` `CommSemiring.toSemiring` `Ring.toIntAlgebra` `CommRing.toRing` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `jacobiSum`	—	`Subalgebra.sum_mem` `Subalgebra.mul_mem` `MulChar.apply_mem_algebraAdjoin_of_pow_eq_one` `Finite.of_fintype`
`jacobiSum_mul_jacobiSum_inv` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `jacobiSum` `MulChar` `CommRing.toCommMonoid` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `MulChar.hasInv` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Fintype.card`	—	`FiniteField.card` `ringChar.charP` `Finite.of_fintype` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `jacobiSum_ringHomComp` `MulChar.ringHomComp_mul` `MulChar.ringHomComp_ne_one_iff` `mul_inv` `inv_ne_one` `Algebra.ringChar_eq` `CharP.ringChar_of_prime_eq_zero` `Nat.cast_pow` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `Eq.trans_ne` `gaussSum_mul_gaussSum_eq_card` `AddChar.PrimitiveAddChar.prim` `mul_right_injective₀` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `mul_mul_mul_comm` `jacobiSum_mul_nontrivial` `MulChar.ringHomComp_inv` `map_natCast`
`jacobiSum_mul_nontrivial` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `gaussSum` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MulChar` `CommRing.toCommMonoid` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `MulChar.hasMul` `jacobiSum`	—	`gaussSum_mul` `Finset.sum_eq_sum_diff_singleton_add` `Finset.mem_univ` `zero_sub` `neg_eq_neg_one_mul` `map_mul` `MonoidHomClass.toMulHomClass` `MulCharClass.toMonoidHomClass` `MulChar.instMulCharClass` `mul_left_comm` `MulChar.mul_apply` `AddChar.map_zero_eq_one` `mul_one` `Finset.mul_sum` `MulChar.sum_eq_zero_of_ne_one` `MulZeroClass.mul_zero` `add_zero` `Equiv.sum_comp` `Finset.sum_congr` `mul_assoc` `mul_comm` `mul_right_comm` `jacobiSum.eq_1` `Finset.sum_mul` `gaussSum.eq_1` `MulChar.map_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `MulZeroClass.zero_mul`
`jacobiSum_nontrivial_inv` 📖	mathematical	—	`jacobiSum` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MulChar` `CommRing.toCommMonoid` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `MulChar.hasInv` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `DFunLike.coe` `MulChar.instFunLike` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`jacobiSum.eq_1` `MulChar.inv_apply'` `map_mul` `MonoidHomClass.toMulHomClass` `MulCharClass.toMonoidHomClass` `MulChar.instMulCharClass` `div_eq_mul_inv` `Finset.sum_eq_sum_diff_singleton_add` `Finset.mem_univ` `sub_self` `div_zero` `MulChar.map_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `add_zero` `Finset.sum_bij'` `div_eq_iff` `sub_ne_zero` `mul_sub` `mul_one` `neg_one_mul` `sub_neg_eq_add` `right_eq_add` `AddRightCancelSemigroup.toIsRightCancelAdd` `neg_eq_zero` `one_ne_zero` `NeZero.one` `eq_neg_of_add_eq_zero_right` `one_mul` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `sub_eq_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `sub_add_cancel` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `GroupWithZero.toNontrivial` `neg_eq_iff_eq_neg` `add_sub_cancel_right` `add_eq_zero_iff_eq_neg` `MulChar.sum_eq_zero_of_ne_one`
`jacobiSum_one_nontrivial` 📖	mathematical	—	`jacobiSum` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MulChar` `CommRing.toCommMonoid` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `MulChar.hasOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Finset.sum_eq_zero` `MulChar.one_apply` `sub_self` `MulZeroClass.zero_mul` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `MulChar.sum_one_eq_card_units` `MulChar.sum_eq_zero_of_ne_one` `add_zero` `Fintype.card_eq_card_units_add_one` `Nat.cast_add` `Nat.cast_one` `sub_add_cancel_left`
`jacobiSum_one_one` 📖	mathematical	—	`jacobiSum` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MulChar` `CommRing.toCommMonoid` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `MulChar.hasOne` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Fintype.card` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat`	—	`jacobiSum_trivial_trivial`
`jacobiSum_ringHomComp` 📖	mathematical	—	`jacobiSum` `MulChar.ringHomComp` `CommRing.toCommMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	—	`Finset.sum_congr` `map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`
`jacobiSum_trivial_trivial` 📖	mathematical	—	`jacobiSum` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MulChar.trivial` `CommRing.toCommMonoid` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Fintype.card` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `jacobiSum_eq_sum_sdiff` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `map_mul` `MonoidHomClass.toMulHomClass` `MulCharClass.toMonoidHomClass` `MulChar.instMulCharClass` `MulChar.trivial_apply` `IsDomain.to_noZeroDivisors` `instIsDomain` `Finset.sum_congr` `Finset.cast_card` `Finset.card_sdiff_of_subset` `Finset.subset_univ` `Finset.card_univ` `Finset.card_pair` `zero_ne_one` `NeZero.one` `Nat.cast_sub` `Fintype.one_lt_card` `Nat.cast_two`

---

← Back to Index