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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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	—	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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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	—	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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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	—	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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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	—	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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nat.instMonoid Distrib.toMul 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.toPow 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	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing	—	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	63 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, 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.toPow 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	add_pow_expChar_of_commute expChar_prime
add_pow_char_pow 📖	mathematical	—	Monoid.toPow 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nat.instMonoid	—	add_pow_expChar_pow_of_commute expChar_prime
add_pow_eq_mul_pow_add_pow_div_char 📖	mathematical	—	Monoid.toPow 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul	—	add_pow_eq_mul_pow_add_pow_div_expChar_of_commute expChar_prime
add_pow_eq_mul_pow_add_pow_div_expChar 📖	mathematical	—	Monoid.toPow 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul	—	add_pow_expChar_of_commute pow_mul pow_add
add_pow_expChar 📖	mathematical	—	Monoid.toPow 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	pow_one Commute.exists_add_pow_prime_eq CharP.cast_eq_zero MulZeroClass.zero_mul add_zero
add_pow_expChar_pow 📖	mathematical	—	Monoid.toPow 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	sub_pow_eq_mul_pow_sub_pow_div_expChar_of_commute expChar_prime
sub_pow_eq_mul_pow_sub_pow_div_expChar 📖	mathematical	—	Monoid.toPow 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	sub_pow_expChar_of_commute pow_mul pow_add
sub_pow_expChar 📖	mathematical	—	Monoid.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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