Multiplicity

📁 Source: Mathlib/NumberTheory/Multiplicity.lean

Statistics

Metric	Count
Definitions	0
Theorems eight_dvd_sq_sub_one_of_odd, emultiplicity_pow_add_pow, emultiplicity_pow_sub_pow, sq_mod_four_eq_one_of_odd, two_pow_sub_pow, two_pow_sub_pow', two_pow_two_pow_add_two_pow_two_pow, two_pow_two_pow_sub_pow_two_pow, eight_dvd_sq_sub_one_of_odd, emultiplicity_pow_add_pow, emultiplicity_pow_sub_pow, two_pow_sub_pow, dvd_geom_sum₂_iff_of_dvd_sub, dvd_geom_sum₂_iff_of_dvd_sub', dvd_geom_sum₂_self, emultiplicity_geom_sum₂_eq_one, emultiplicity_pow_prime_pow_sub_pow_prime_pow, emultiplicity_pow_prime_sub_pow_prime, emultiplicity_pow_sub_pow_of_prime, not_dvd_geom_sum₂, odd_sq_dvd_geom_sum₂_sub, pow_add_pow, pow_sub_pow, pow_two_sub_one, pow_two_sub_one_ge, pow_two_sub_pow, pow_two_pow_sub_pow_two_pow, sq_dvd_add_pow_sub_sub	28
Total	28

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eight_dvd_sq_sub_one_of_odd 📖	mathematical	Odd instSemiring	Monoid.toNatPow instMonoid	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt 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.one_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.pow_zero 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add mul_dvd_mul_iff_left IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero four_ne_zero two_dvd_mul_add_one
emultiplicity_pow_add_pow 📖	mathematical	Nat.Prime Odd Nat.instSemiring	emultiplicity instMonoid Monoid.toNatPow ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instMonoid	—	sub_neg_eq_add Odd.neg_pow emultiplicity_pow_sub_pow
emultiplicity_pow_sub_pow 📖	mathematical	Nat.Prime Odd Nat.instSemiring	emultiplicity instMonoid Monoid.toNatPow ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instMonoid	—	pow_zero sub_self emultiplicity_zero add_top Nat.finiteMultiplicity_iff Nat.Prime.ne_one emultiplicity_eq_coe FiniteMultiplicity.emultiplicity_eq_multiplicity pow_mul emultiplicity_pow_sub_pow_of_prime instIsDomain Nat.prime_iff_prime_int geom_sum₂_mul Prime.dvd_of_dvd_pow pow_succ mul_assoc emultiplicity_pow_prime_pow_sub_pow_prime_pow
sq_mod_four_eq_one_of_odd 📖	mathematical	Odd instSemiring	Monoid.toNatPow instMonoid	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt 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.one_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one add_zero Mathlib.Tactic.RingNF.add_assoc_rev add_assoc add_mul Distrib.rightDistribClass
two_pow_sub_pow 📖	mathematical	Even	ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat emultiplicity instMonoid Monoid.toNatPow AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	even_neg Nat.instAtLeastTwoHAddOfNat even_iff_two_dvd Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.term_add_constg Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add zero_add Mathlib.Tactic.Abel.zero_termg Even.add_odd not_even_iff_odd pow_mul sq_mod_four_eq_one_of_odd sub_self two_pow_sub_pow' Odd.pow sq_sub_sq emultiplicity_mul instIsCancelMulZero prime_two Nat.cast_one natCast_emultiplicity FiniteMultiplicity.emultiplicity_self Nat.instIsCancelMulZero Nat.finiteMultiplicity_iff add_comm add_assoc
two_pow_sub_pow' 📖	mathematical	—	emultiplicity instMonoid Monoid.toNatPow ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	not_even_iff_odd Nat.instAtLeastTwoHAddOfNat even_iff_two_dvd dvd_trans sub_sub_cancel Odd.sub_even pow_zero sub_self emultiplicity_zero add_top Nat.finiteMultiplicity_iff Nat.instCharZero emultiplicity_eq_coe FiniteMultiplicity.emultiplicity_eq_multiplicity pow_mul emultiplicity_pow_sub_pow_of_prime instIsDomain prime_two Odd.sub_odd Odd.pow Mathlib.Tactic.Contrapose.contrapose₄ pow_succ mul_dvd_mul_left two_pow_two_pow_sub_pow_two_pow natCast_emultiplicity
two_pow_two_pow_add_two_pow_two_pow 📖	mathematical	—	emultiplicity instMonoid Monoid.toNatPow Nat.instMonoid ENat ENat.instNatCast	—	not_even_iff_odd Nat.instAtLeastTwoHAddOfNat even_iff_two_dvd dvd_trans sub_sub_cancel Odd.sub_even emultiplicity_eq_coe pow_one Odd.add_odd Odd.pow pow_succ' mul_comm pow_mul sq_mod_four_eq_one_of_odd
two_pow_two_pow_sub_pow_two_pow 📖	mathematical	—	emultiplicity instMonoid Monoid.toNatPow Nat.instMonoid ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ENat.instNatCast	—	pow_two_pow_sub_pow_two_pow emultiplicity_mul instIsCancelMulZero prime_two Finset.emultiplicity_prod Finset.sum_congr two_pow_two_pow_add_two_pow_two_pow Nat.cast_one Finset.sum_const Finset.card_range nsmul_one add_comm

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eight_dvd_sq_sub_one_of_odd 📖	mathematical	Odd instSemiring	Monoid.toNatPow instMonoid	—	mul_dvd_mul_iff_left IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero four_ne_zero two_dvd_mul_add_one
emultiplicity_pow_add_pow 📖	mathematical	Prime Odd instSemiring	emultiplicity instMonoid Monoid.toNatPow ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	Int.natCast_emultiplicity cast_add cast_pow Int.emultiplicity_pow_add_pow
emultiplicity_pow_sub_pow 📖	mathematical	Prime Odd instSemiring	emultiplicity instMonoid Monoid.toNatPow ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	le_total Int.natCast_emultiplicity cast_pow Int.emultiplicity_pow_sub_pow emultiplicity_zero top_add
two_pow_sub_pow 📖	mathematical	Even	ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat emultiplicity instMonoid Monoid.toNatPow AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	le_total Int.natCast_emultiplicity pow_le_pow_left' instMulLeftMono covariant_swap_mul_of_covariant_mul Int.two_pow_sub_pow emultiplicity_zero top_add add_top

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvd_geom_sum₂_iff_of_dvd_sub 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne	—	Ideal.instIsTwoSided_1 RingHom.map_geom_sum₂ Finset.sum_congr Ideal.Quotient.eq Ideal.mem_span_singleton geom_sum₂_self map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_natCast map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
dvd_geom_sum₂_iff_of_dvd_sub' 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne	—	geom_sum₂_comm dvd_geom_sum₂_iff_of_dvd_sub neg_sub Dvd.dvd.neg_right
dvd_geom_sum₂_self 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	dvd_geom_sum₂_iff_of_dvd_sub dvd_mul_right
emultiplicity_geom_sum₂_eq_one 📖	mathematical	Prime CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Odd Nat.instSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	emultiplicity MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instCommSemiringENat	—	Nat.cast_one emultiplicity_eq_coe pow_one dvd_geom_sum₂_self Nat.instAtLeastTwoHAddOfNat one_add_one_eq_two eq_add_of_sub_eq' dvd_iff_dvd_of_dvd_sub odd_sq_dvd_geom_sum₂_sub pow_two mul_dvd_mul_iff_left IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Prime.ne_zero Prime.dvd_of_dvd_pow
emultiplicity_pow_prime_pow_sub_pow_prime_pow 📖	mathematical	Prime CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Odd Nat.instSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	emultiplicity MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Monoid.toNatPow Nat.instMonoid ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instCommSemiringENat ENat.instNatCast	—	Nat.cast_zero add_zero pow_zero pow_one Nat.cast_add Nat.cast_one add_assoc pow_succ pow_mul emultiplicity_pow_prime_sub_pow_prime geom_sum₂_mul dvd_mul_of_dvd_right Prime.dvd_of_dvd_pow
emultiplicity_pow_prime_sub_pow_prime 📖	mathematical	Prime CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Odd Nat.instSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	emultiplicity MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Monoid.toNatPow ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instCommSemiringENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	geom_sum₂_mul emultiplicity_mul IsDomain.toIsCancelMulZero emultiplicity_geom_sum₂_eq_one add_comm
emultiplicity_pow_sub_pow_of_prime 📖	mathematical	Prime CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne	emultiplicity MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Monoid.toNatPow	—	geom_sum₂_mul emultiplicity_mul IsDomain.toIsCancelMulZero emultiplicity_eq_zero not_dvd_geom_sum₂ zero_add
not_dvd_geom_sum₂ 📖	mathematical	Prime CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	—	Prime.dvd_of_dvd_pow Prime.dvd_or_dvd dvd_geom_sum₂_iff_of_dvd_sub'
odd_sq_dvd_geom_sum₂_sub 📖	mathematical	Odd Nat.instSemiring	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd	—	instIsTransDvd mul_pow sq_dvd_add_pow_sub_sub Ideal.instIsTwoSided_1 Finset.sum_congr RingHom.map_geom_sum₂ MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero Mathlib.Tactic.Ring.atom_pf' RingHomClass.toAddMonoidHomClass Finset.sum_add_distrib map_add AddMonoidHomClass.toAddHomClass AddLeftCancelSemigroup.toIsLeftCancelAdd Finset.mem_range Finset.sum_const Finset.card_range nsmul_eq_mul Finset.mul_sum Nat.cast_zero MulZeroClass.mul_zero Mathlib.Tactic.Ring.of_eq Nat.cast_sum AddRightCancelSemigroup.toIsRightCancelAdd Finset.sum_range_id Nat.instAtLeastTwoHAddOfNat even_iff_two_dvd Nat.Odd.sub_odd odd_one Nat.cast_mul map_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw mul_assoc mul_eq_zero_of_left Ideal.Quotient.eq_zero_iff_mem
pow_two_pow_sub_pow_two_pow 📖	mathematical	—	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Nat.instMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.prod CommRing.toCommMonoid Finset.range Distrib.toAdd	—	pow_zero pow_one one_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Finset.prod_range_succ mul_assoc mul_comm
sq_dvd_add_pow_sub_sub 📖	mathematical	—	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing Distrib.toMul AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne	—	pow_zero Nat.cast_zero MulZeroClass.mul_zero sub_zero sub_self add_pow Finset.sum_range_succ add_tsub_cancel_left Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid pow_one Nat.choose_succ_self_right Nat.cast_succ tsub_self Nat.instCanonicallyOrderedAdd mul_one Nat.choose_self zero_add tsub_zero Finset.dvd_sum instIsTransDvd pow_dvd_pow le_tsub_of_add_le_left le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing Nat.cast_add Nat.cast_one Finset.mem_range dvd_mul_of_dvd_left dvd_mul_left Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isInt_neg add_zero Mathlib.Tactic.Abel.zero_termg

padicValNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pow_add_pow 📖	mathematical	Odd Nat.instSemiring	padicValNat Monoid.toNatPow Nat.instMonoid	—	Nat.cast_add padicValNat_eq_emultiplicity LT.lt.ne' pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass Nat.instCanonicallyOrderedAdd Odd.pos Nat.instNontrivial Nat.emultiplicity_pow_add_pow Fact.out
pow_sub_pow 📖	mathematical	Odd Nat.instSemiring	padicValNat Monoid.toNatPow Nat.instMonoid	—	Nat.cast_add padicValNat_eq_emultiplicity Nat.emultiplicity_pow_sub_pow Fact.out
pow_two_sub_one 📖	mathematical	Even	padicValNat Monoid.toNatPow Nat.instMonoid	—	one_pow pow_two_sub_pow
pow_two_sub_one_ge 📖	mathematical	Even	padicValNat Monoid.toNatPow Nat.instMonoid	—	padicValNat_dvd_iff_le Nat.fact_prime_two one_pow pow_two_sub_one
pow_two_sub_pow 📖	mathematical	Even	padicValNat Monoid.toNatPow Nat.instMonoid	—	Nat.cast_add padicValNat_eq_emultiplicity Nat.fact_prime_two Nat.instCanonicallyOrderedAdd Nat.instOrderedSub Nat.two_pow_sub_pow

---

← Back to Index