ModEq

📁 Source: Mathlib/Algebra/BigOperators/ModEq.lean

Statistics

Metric	Count
Definitions	0
Theorems listProd_map, listProd_map_one, listProd_one, listSum_map, listSum_map_zero, listSum_zero, multisetProd_map, multisetProd_map_one, multisetProd_one, multisetSum_map, multisetSum_map_zero, multisetSum_zero, prod, prod_one, sum, sum_zero, prod_modEq_ite, prod_modEq_single, sum_modEq_ite, sum_modEq_single, listProd_map, listProd_map_one, listProd_one, listSum_map, listSum_map_zero, listSum_zero, multisetProd_map, multisetProd_map_one, multisetProd_one, multisetSum_map, multisetSum_map_zero, multisetSum_zero, prod, prod_one, sum, sum_zero, prod_modEq_ite, prod_modEq_single, sum_modEq_ite, sum_modEq_single	40
Total	40

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_modEq_ite 📖	mathematical	ModEq	Finset.prod instCommMonoid Finset Finset.instMembership Finset.decidableMem	—	modEq_natAbs cast_prod cast_one Finset.prod_eq_ite
prod_modEq_single 📖	mathematical	ModEq	Finset.prod instCommMonoid	—	modEq_natAbs cast_prod Finset.prod_eq_single cast_one
sum_modEq_ite 📖	mathematical	ModEq	Finset.sum instAddCommMonoid Finset Finset.instMembership Finset.decidableMem	—	modEq_natAbs cast_sum cast_zero Finset.sum_eq_ite
sum_modEq_single 📖	mathematical	ModEq	Finset.sum instAddCommMonoid	—	modEq_natAbs cast_sum Finset.sum_eq_single cast_zero

Int.ModEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
listProd_map 📖	mathematical	Int.ModEq	AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	mul
listProd_map_one 📖	mathematical	Int.ModEq	AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	trans listProd_map List.prod_replicate one_pow
listProd_one 📖	mathematical	Int.ModEq	AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	listProd_map_one
listSum_map 📖	mathematical	Int.ModEq	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	add
listSum_map_zero 📖	mathematical	Int.ModEq	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	List.sum_replicate nsmul_zero listSum_map
listSum_zero 📖	mathematical	Int.ModEq	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	listSum_map_zero
multisetProd_map 📖	mathematical	Int.ModEq	Multiset.prod Int.instCommMonoid Multiset.map	—	listProd_map
multisetProd_map_one 📖	mathematical	Int.ModEq	Multiset.prod Int.instCommMonoid Multiset.map	—	Multiset.map_const' Multiset.prod_replicate one_pow multisetProd_map
multisetProd_one 📖	mathematical	Int.ModEq	Multiset.prod Int.instCommMonoid	—	Multiset.map_id' multisetProd_map_one
multisetSum_map 📖	mathematical	Int.ModEq	Multiset.sum Int.instAddCommMonoid Multiset.map	—	listSum_map
multisetSum_map_zero 📖	mathematical	Int.ModEq	Multiset.sum Int.instAddCommMonoid Multiset.map	—	Multiset.map_const' Multiset.sum_replicate nsmul_zero multisetSum_map
multisetSum_zero 📖	mathematical	Int.ModEq	Multiset.sum Int.instAddCommMonoid	—	Multiset.map_id' multisetSum_map_zero
prod 📖	mathematical	Int.ModEq	Finset.prod Int.instCommMonoid	—	multisetProd_map
prod_one 📖	mathematical	Int.ModEq	Finset.prod Int.instCommMonoid	—	Finset.prod_const_one prod
sum 📖	mathematical	Int.ModEq	Finset.sum Int.instAddCommMonoid	—	multisetSum_map
sum_zero 📖	mathematical	Int.ModEq	Finset.sum Int.instAddCommMonoid	—	multisetSum_map_zero

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_modEq_ite 📖	mathematical	ModEq	Finset.prod instCommMonoid Finset Finset.instMembership Finset.decidableMem	—	cast_prod cast_one Finset.prod_eq_ite
prod_modEq_single 📖	mathematical	ModEq	Finset.prod instCommMonoid	—	cast_prod Finset.prod_eq_single cast_one
sum_modEq_ite 📖	mathematical	ModEq	Finset.sum instAddCommMonoid Finset Finset.instMembership Finset.decidableMem	—	cast_sum cast_zero Finset.sum_eq_ite
sum_modEq_single 📖	mathematical	ModEq	Finset.sum instAddCommMonoid	—	cast_sum Finset.sum_eq_single cast_zero

Nat.ModEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
listProd_map 📖	mathematical	Nat.ModEq	Nat.instOne	—	mul
listProd_map_one 📖	mathematical	Nat.ModEq	Nat.instOne	—	trans listProd_map List.prod_replicate one_pow
listProd_one 📖	mathematical	Nat.ModEq	Nat.instOne	—	listProd_map_one
listSum_map 📖	mathematical	Nat.ModEq	MulZeroClass.toZero Nat.instMulZeroClass	—	—
listSum_map_zero 📖	mathematical	Nat.ModEq	MulZeroClass.toZero Nat.instMulZeroClass	—	List.sum_replicate nsmul_zero listSum_map
listSum_zero 📖	mathematical	Nat.ModEq	MulZeroClass.toZero Nat.instMulZeroClass	—	List.sum_replicate nsmul_zero listSum_map
multisetProd_map 📖	mathematical	Nat.ModEq	Multiset.prod Nat.instCommMonoid Multiset.map	—	listProd_map
multisetProd_map_one 📖	mathematical	Nat.ModEq	Multiset.prod Nat.instCommMonoid Multiset.map	—	Multiset.map_const' Multiset.prod_replicate one_pow multisetProd_map
multisetProd_one 📖	mathematical	Nat.ModEq	Multiset.prod Nat.instCommMonoid	—	Multiset.map_id' multisetProd_map_one
multisetSum_map 📖	mathematical	Nat.ModEq	Multiset.sum Nat.instAddCommMonoid Multiset.map	—	listSum_map
multisetSum_map_zero 📖	mathematical	Nat.ModEq	Multiset.sum Nat.instAddCommMonoid Multiset.map	—	Multiset.map_const' Multiset.sum_replicate nsmul_zero multisetSum_map
multisetSum_zero 📖	mathematical	Nat.ModEq	Multiset.sum Nat.instAddCommMonoid	—	Multiset.map_id' Multiset.map_const' Multiset.sum_replicate nsmul_zero multisetSum_map
prod 📖	mathematical	Nat.ModEq	Finset.prod Nat.instCommMonoid	—	multisetProd_map
prod_one 📖	mathematical	Nat.ModEq	Finset.prod Nat.instCommMonoid	—	Finset.prod_const_one prod
sum 📖	mathematical	Nat.ModEq	Finset.sum Nat.instAddCommMonoid	—	multisetSum_map
sum_zero 📖	mathematical	Nat.ModEq	Finset.sum Nat.instAddCommMonoid	—	Finset.sum_const_zero sum

---

← Back to Index