Lemmas

📁 Source: Mathlib/Algebra/CharP/Lemmas.lean

Statistics

Metric	Count
Definitions frobenius, iterateFrobenius	2
Theorems char_is_prime, char_ne_zero_of_finite, prime_ringChar, ringChar_ne_zero_of_finite, add_pow_prime_eq, add_pow_prime_eq', add_pow_prime_pow_eq, add_pow_prime_pow_eq', exists_add_pow_prime_eq, exists_add_pow_prime_pow_eq, dvd_add_pow_sub_pow_of_dvd, add_pow_char, add_pow_char_of_commute, add_pow_char_pow, add_pow_char_pow_of_commute, add_pow_eq_mul_pow_add_pow_div_char, add_pow_eq_mul_pow_add_pow_div_char_of_commute, add_pow_eq_mul_pow_add_pow_div_expChar, add_pow_eq_mul_pow_add_pow_div_expChar_of_commute, add_pow_expChar, add_pow_expChar_of_commute, add_pow_expChar_pow, add_pow_expChar_pow_of_commute, add_pow_prime_eq, add_pow_prime_eq', add_pow_prime_pow_eq, add_pow_prime_pow_eq', exists_add_pow_prime_eq, exists_add_pow_prime_pow_eq, list_sum_pow_char, list_sum_pow_char_pow, multiset_sum_pow_char, multiset_sum_pow_char_pow, neg_one_pow_char, neg_one_pow_char_pow, neg_one_pow_expChar, neg_one_pow_expChar_pow, sub_pow_char, sub_pow_char_of_commute, sub_pow_char_pow, sub_pow_char_pow_of_commute, sub_pow_eq_mul_pow_sub_pow_div_char, sub_pow_eq_mul_pow_sub_pow_div_char_of_commute, sub_pow_eq_mul_pow_sub_pow_div_expChar, sub_pow_eq_mul_pow_sub_pow_div_expChar_of_commute, sub_pow_expChar, sub_pow_expChar_of_commute, sub_pow_expChar_pow, sub_pow_expChar_pow_of_commute, sum_pow_char, sum_pow_char_pow	51
Total	53

CharP

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
char_is_prime 📖	mathematical	—	Nat.Prime	—	char_is_prime_or_zero char_ne_zero_of_finite
char_ne_zero_of_finite 📖	—	—	—	—	Nat.cast_injective charP_to_charZero not_injective_infinite_finite instInfiniteNat
prime_ringChar 📖	mathematical	—	Nat.Prime ringChar Semiring.toNonAssocSemiring Ring.toSemiring	—	char_prime_of_ne_zero ringChar.charP ringChar_ne_zero_of_finite
ringChar_ne_zero_of_finite 📖	—	—	—	—	char_ne_zero_of_finite ringChar.charP

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_pow_prime_eq 📖	mathematical	Nat.Prime Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.Ioo Nat.instPreorder Nat.instLocallyFiniteOrder Nat.choose	—	pow_one Finset.sum_congr add_pow_prime_pow_eq
add_pow_prime_eq' 📖	mathematical	Nat.Prime Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.Ioo Nat.instPreorder Nat.instLocallyFiniteOrder Nat.choose	—	pow_one Finset.sum_congr add_pow_prime_pow_eq'
add_pow_prime_pow_eq 📖	mathematical	Nat.Prime Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd Nat.instMonoid AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.Ioo Nat.instPreorder Nat.instLocallyFiniteOrder Nat.choose	—	add_pow_prime_pow_eq' mul_assoc Finset.mul_sum Finset.sum_congr Finset.mem_Ioo mul_pow_sub_one mul_mul_mul_comm pow_left
add_pow_prime_pow_eq' 📖	mathematical	Nat.Prime Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd Nat.instMonoid AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.Ioo Nat.instPreorder Nat.instLocallyFiniteOrder Nat.choose	—	add_pow Nat.Ico_zero_eq_range Finset.Ico_add_one_right_eq_Icc Nat.instNoMaxOrder Finset.right_notMem_Ico Finset.sum_congr Finset.Icc_eq_cons_Ico zero_le Nat.instCanonicallyOrderedAdd Finset.left_notMem_Ioo Finset.Ico_eq_cons_Ioo pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass Nat.Prime.pos Finset.cons.congr_simp Finset.sum_cons tsub_self Nat.instOrderedSub pow_zero mul_one Nat.choose_self Nat.cast_one tsub_zero one_mul Nat.choose_zero_right add_assoc Finset.mul_sum Finset.mem_Ioo Nat.cast_comm mul_assoc Nat.Prime.dvd_choose_pow
exists_add_pow_prime_eq 📖	mathematical	Nat.Prime Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	add_pow_prime_eq
exists_add_pow_prime_pow_eq 📖	mathematical	Nat.Prime Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd Nat.instMonoid AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	add_pow_prime_pow_eq

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvd_add_pow_sub_pow_of_dvd 📖	mathematical	Nat.Prime semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Distrib.toAdd	—	add_pow_prime_eq add_right_comm add_assoc add_sub_assoc add_sub_cancel_right dvd_add Distrib.leftDistribClass Dvd.dvd.trans dvd_mul_right

(root)

Definitions

Name	Category	Theorems
frobenius 📖	CompOp	64 math math: Perfection.pthRoot_frobenius, frobeniusEquiv_apply, coe_frobeniusEquiv_symm_comp_coe_frobenius, PerfectClosure.mk_mul_mk, frobenius_one, frobenius_natCast, PerfectClosure.frobenius_mk, Polynomial.Monic.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one, frobeniusEquiv_symm_comp_frobenius, MonoidHom.map_iterate_frobenius, RingHom.frobenius_comm, MvPolynomial.map_frobenius_expand, injective_frobenius, MvPolynomial.expand_char, frobenius_mul, PerfectRing.bijective_frobenius, minpoly.frobenius_of_isSeparable, Polynomial.roots_expand_map_frobenius, Polynomial.roots_expand_image_frobenius, PerfectClosure.mk_add_mk, MonoidHom.iterate_map_frobenius, frobenius_sub, WittVector.frobenius_eq_map_frobenius, frobenius_zero, RingHom.map_iterate_frobenius, PreTilt.coeff_frobenius, Polynomial.roots_expand_image_frobenius_subset, Perfection.coeff_iterate_frobenius, coe_frobeniusEquiv, frobenius_comp_frobeniusEquiv_symm, coe_frobenius_comp_coe_frobeniusEquiv_symm, MvPolynomial.frobenius_zmod, frobenius_neg, RingHom.iterate_map_frobenius, coe_iterateFrobenius, iterate_frobenius, frobenius_def, surjective_frobenius, bijective_frobenius, PerfectClosure.mk_eq_iff, PerfectClosure.r_iff, ZMod.frobenius_zmod, iterateFrobenius_one, frobenius_apply_frobeniusEquiv_symm, MvPowerSeries.map_frobenius_expand, PreTilt.coeff_iterate_frobenius, Polynomial.Monic.eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible, LinearMap.frobenius_def, FiniteField.frobenius_pow, Polynomial.expand_char, iterateFrobenius_eq_pow, Polynomial.map_frobenius_expand, PerfectClosure.iterate_frobenius_mk, PerfectClosure.eq_iff, MonoidHom.map_frobenius, frobenius_add, Perfection.coeff_iterate_frobenius', RingHom.map_frobenius, Polynomial.roots_expand_map_frobenius_le, Perfection.frobenius_pthRoot, PreTilt.coeff_iterate_frobenius', frobeniusEquiv_symm_apply_frobenius, Perfection.coeff_frobenius, frobenius_inj
iterateFrobenius 📖	CompOp	32 math math: coe_iterateFrobenius_mul, bijective_iterateFrobenius, iterateFrobenius_one_apply, LinearMap.iterateFrobenius_def, iterateFrobenius_inj, MvPolynomial.map_expand_pow_char, iterateFrobenius_zero, iterateFrobenius_def, Polynomial.roots_expand_pow_map_iterateFrobenius_le, iterateFrobenius_add, coe_iterateFrobenius, RingHom.map_iterateFrobenius, Polynomial.roots_expand_pow_map_iterateFrobenius, Polynomial.map_expand_pow_char, MvPowerSeries.map_iterateFrobenius_expand, iterateFrobeniusEquiv_apply, MonoidHom.map_iterateFrobenius, MvPolynomial.map_iterateFrobenius_expand, iterateFrobenius_one, Polynomial.roots_expand_image_iterateFrobenius, Polynomial.roots_expand_pow_image_iterateFrobenius_subset, iterateFrobenius_eq_pow, IsPurelyInseparable.iterateFrobeniusₛₗ_algebraMap, IsPurelyInseparable.iterateFrobeniusₛₗ_algebraMap_base, minpoly.iterateFrobenius_of_isSeparable, iterateFrobenius_add_apply, coe_iterateFrobeniusEquiv, RingHom.iterateFrobenius_comm, iterateFrobenius_zero_apply, iterateFrobenius_mul_apply, IsPurelyInseparable.algebraMap_iterateFrobeniusₛₗ, Polynomial.map_iterateFrobenius_expand

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_pow_char 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	add_pow_expChar expChar_prime
add_pow_char_of_commute 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd	—	add_pow_expChar_of_commute expChar_prime
add_pow_char_pow 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nat.instMonoid	—	add_pow_expChar_pow expChar_prime
add_pow_char_pow_of_commute 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd Nat.instMonoid	—	add_pow_expChar_pow_of_commute expChar_prime
add_pow_eq_mul_pow_add_pow_div_char 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul	—	add_pow_eq_mul_pow_add_pow_div_expChar expChar_prime
add_pow_eq_mul_pow_add_pow_div_char_of_commute 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd	—	add_pow_eq_mul_pow_add_pow_div_expChar_of_commute expChar_prime
add_pow_eq_mul_pow_add_pow_div_expChar 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul	—	add_pow_eq_mul_pow_add_pow_div_expChar_of_commute Commute.all
add_pow_eq_mul_pow_add_pow_div_expChar_of_commute 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd	—	add_pow_expChar_of_commute pow_mul pow_add
add_pow_expChar 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	add_pow_expChar_of_commute Commute.all
add_pow_expChar_of_commute 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd	—	pow_one Commute.exists_add_pow_prime_eq CharP.cast_eq_zero MulZeroClass.zero_mul add_zero
add_pow_expChar_pow 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nat.instMonoid	—	add_pow_expChar_pow_of_commute Commute.all
add_pow_expChar_pow_of_commute 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd Nat.instMonoid	—	one_pow pow_one Commute.exists_add_pow_prime_pow_eq CharP.cast_eq_zero MulZeroClass.zero_mul add_zero
add_pow_prime_eq 📖	mathematical	Nat.Prime	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.Ioo Nat.instPreorder Nat.instLocallyFiniteOrder Nat.choose	—	Commute.add_pow_prime_eq Commute.all
add_pow_prime_eq' 📖	mathematical	Nat.Prime	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.Ioo Nat.instPreorder Nat.instLocallyFiniteOrder Nat.choose	—	Commute.add_pow_prime_eq' Commute.all
add_pow_prime_pow_eq 📖	mathematical	Nat.Prime	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nat.instMonoid Distrib.toMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.Ioo Nat.instPreorder Nat.instLocallyFiniteOrder Nat.choose	—	Commute.add_pow_prime_pow_eq Commute.all
add_pow_prime_pow_eq' 📖	mathematical	Nat.Prime	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nat.instMonoid Distrib.toMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.Ioo Nat.instPreorder Nat.instLocallyFiniteOrder Nat.choose	—	Commute.add_pow_prime_pow_eq' Commute.all
exists_add_pow_prime_eq 📖	mathematical	Nat.Prime	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Commute.exists_add_pow_prime_eq Commute.all
exists_add_pow_prime_pow_eq 📖	mathematical	Nat.Prime	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nat.instMonoid Distrib.toMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Commute.exists_add_pow_prime_pow_eq Commute.all
list_sum_pow_char 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	map_list_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
list_sum_pow_char_pow 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Nat.instMonoid	—	map_list_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
multiset_sum_pow_char 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Multiset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Multiset.map	—	map_multiset_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
multiset_sum_pow_char_pow 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Multiset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nat.instMonoid Multiset.map	—	map_multiset_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
neg_one_pow_char 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	neg_one_pow_expChar expChar_prime
neg_one_pow_char_pow 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instMonoid	—	neg_one_pow_expChar_pow expChar_prime
neg_one_pow_expChar 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	eq_neg_iff_add_eq_zero one_pow add_pow_expChar_of_commute Commute.one_right neg_add_cancel zero_pow expChar_ne_zero
neg_one_pow_expChar_pow 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instMonoid	—	eq_neg_iff_add_eq_zero one_pow add_pow_expChar_pow_of_commute Commute.one_right neg_add_cancel zero_pow pow_ne_zero isReduced_of_noZeroDivisors IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd expChar_ne_zero
sub_pow_char 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	sub_pow_expChar expChar_prime
sub_pow_char_of_commute 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	sub_pow_expChar_of_commute expChar_prime
sub_pow_char_pow 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Nat.instMonoid	—	sub_pow_expChar_pow expChar_prime
sub_pow_char_pow_of_commute 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Nat.instMonoid	—	sub_pow_expChar_pow_of_commute expChar_prime
sub_pow_eq_mul_pow_sub_pow_div_char 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	sub_pow_eq_mul_pow_sub_pow_div_expChar expChar_prime
sub_pow_eq_mul_pow_sub_pow_div_char_of_commute 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	sub_pow_eq_mul_pow_sub_pow_div_expChar_of_commute expChar_prime
sub_pow_eq_mul_pow_sub_pow_div_expChar 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	sub_pow_eq_mul_pow_sub_pow_div_expChar_of_commute Commute.all
sub_pow_eq_mul_pow_sub_pow_div_expChar_of_commute 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	sub_pow_expChar_of_commute pow_mul pow_add
sub_pow_expChar 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	sub_pow_expChar_of_commute Commute.all
sub_pow_expChar_of_commute 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	add_pow_expChar_of_commute Commute.sub_left sub_add_cancel
sub_pow_expChar_pow 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Nat.instMonoid	—	sub_pow_expChar_pow_of_commute Commute.all
sub_pow_expChar_pow_of_commute 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Nat.instMonoid	—	add_pow_expChar_pow_of_commute Commute.sub_left sub_add_cancel
sum_pow_char 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
sum_pow_char_pow 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nat.instMonoid	—	map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass

---

← Back to Index