Basic

📁 Source: Mathlib/RingTheory/DividedPowers/Basic.lean

Statistics

Metric	Count
Definitions DividedPowers, dpow, equiv, exp, ofRingEquiv, dividedPowersBot, instCoeFunDividedPowersForallNatForall, instInhabitedDividedPowersBotIdeal	8
Theorems coe_injective, coincide_on_smul, dpow_add, dpow_add', dpow_comp, dpow_eval_zero, dpow_mem, dpow_mul, dpow_mul_right, dpow_null, dpow_one, dpow_smul, dpow_smul_right, dpow_sum, dpow_sum', dpow_zero, equiv_apply, equiv_apply', exp_add, exp_add', ext, ext_iff, factorial_mul_dpow_eq_pow, mul_dpow, nilpotent_of_mem_dpIdeal, ofRingEquiv_dpow, ofRingEquiv_dpow_apply, prod_dpow, dividedPowersBot_dpow_eq	29
Total	37

DividedPowers

Definitions

Name	Category	Theorems
dpow 📖	CompOp	49 math math: dpow_mem, RatAlgebra.dpow_eq_inv_fact_smul, factorial_mul_dpow_eq_pow, OfInvertibleFactorial.dpow_apply, Quotient.OfSurjective.dpow_def, dpow_null, ext_iff, mem_dpEqualizer_iff, coincide_on_smul, ofRingEquiv_dpow, equiv_apply, dpow_comp, dpow_add, dpow_mul_right, IsSubDPIdeal.dpow_mem, isDPMorphism_iff, DPMorphism.dpow_comp, dpow_sum, RatAlgebra.dpow_apply, IsDPMorphism.map_dpow, mul_dpow, equiv_apply', Quotient.OfSurjective.dpow_apply', dpow_eval_zero, OfSquareZero.dpow_of_two_le, isDPMorphism_def, dpow_mul, SubDPIdeal.dpow_mem, IsSubDPIdeal.dpow_eq_of_mem, dpow_zero, ofRingEquiv_dpow_apply, span_isSubDPIdeal_iff, dividedPowersBot_dpow_eq, IsDPMorphism.dpow_comp, dpow_smul_right, Quotient.OfSurjective.dpow_apply, dpow_add', SubDPIdeal.span_carrier_eq_dpow_span, IsSubDPIdeal.dpow_eq, dpow_one, Quotient.dpow_apply, CharP.dpow_of_prime_le, isSubDPIdeal_inf_iff, prod_dpow, dpow_span_isSubideal, IsNilpotent.dpow_of_prime_le, PadicInt.coe_dpow_eq, dpow_smul, coe_injective
equiv 📖	CompOp	2 math math: equiv_apply, equiv_apply'
exp 📖	CompOp	1 math math: exp_add
ofRingEquiv 📖	CompOp	2 math math: ofRingEquiv_dpow, ofRingEquiv_dpow_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_injective 📖	mathematical	—	DividedPowers dpow	—	ext
coincide_on_smul 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instSMul IsScalarTower.right Algebra.id	dpow	—	IsScalarTower.right Submodule.smul_induction_on' smul_eq_mul dpow_mul mul_comm factorial_mul_dpow_eq_pow Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul dpow_add Ideal.mul_le_right Ideal.instIsTwoSided Ideal.mul_le_left Finset.sum_congr
dpow_add 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	dpow Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Finset.sum Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid Finset.Nat.instHasAntidiagonal Distrib.toMul	—	—
dpow_add' 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	dpow Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Finset.sum Finset.range Distrib.toMul	—	dpow_add
dpow_comp 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	dpow Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.uniformBell	—	—
dpow_eval_zero 📖	mathematical	—	dpow MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	MulZeroClass.mul_zero dpow_mul Ideal.zero_mem zero_pow MulZeroClass.zero_mul
dpow_mem 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	dpow	—	—
dpow_mul 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	dpow Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—
dpow_mul_right 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	dpow Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	mul_comm dpow_mul
dpow_null 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	dpow MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
dpow_one 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	dpow	—	—
dpow_smul 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	dpow Algebra.toSMul Algebra.id Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	dpow_mul
dpow_smul_right 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	dpow Algebra.toSMul Algebra.id Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	smul_eq_mul dpow_mul_right
dpow_sum 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	dpow Finset.sum Sym Finset.sym Finset.prod CommSemiring.toCommMonoid Multiset.count Sym.toMultiset	—	dpow_sum' dpow_zero dpow_add dpow_eval_zero
dpow_sum' 📖	mathematical	AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid Finset.Nat.instHasAntidiagonal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	Sym Finset.sym Finset.prod CommSemiring.toCommMonoid Multiset.count Sym.toMultiset	—	Finset.induction Finset.sum_congr Finset.sum_const nsmul_eq_mul mul_one AddSubmonoid.zero_mem Finset.card_singleton Nat.cast_one Nat.cast_zero Finset.card_eq_zero Finset.sym_eq_empty Finset.mem_insert_of_mem Finset.sum_insert Finset.mem_insert_self AddSubmonoid.sum_mem Finset.sum_range Finset.mul_sum Finset.sum_sigma' Finset.sum_bij' Finset.mem_sigma Finset.mem_univ Finset.erase_insert Finset.sym_filterNe_mem Sym.fill_filterNe Sym.filter_ne_fill Finset.prod_insert Finset.prod_congr Sym.count_coe_fill_of_ne
dpow_zero 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	dpow AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
equiv_apply 📖	mathematical	Ideal.map RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike	dpow DFunLike.coe Equiv DividedPowers Equiv.instEquivLike equiv RingEquiv.symm	—	—
equiv_apply' 📖	mathematical	Ideal.map RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike	dpow DFunLike.coe Equiv DividedPowers Equiv.instEquivLike equiv	—	ofRingEquiv_dpow_apply
exp_add 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	exp Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib PowerSeries MvPowerSeries.instMul	—	exp_add' dpow_add
exp_add' 📖	mathematical	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid Finset.Nat.instHasAntidiagonal Distrib.toMul	PowerSeries MvPowerSeries.instMul	—	PowerSeries.ext Finset.sum_congr PowerSeries.coeff_mul
ext 📖	—	dpow	—	—	—
ext_iff 📖	mathematical	—	dpow	—	ext
factorial_mul_dpow_eq_pow 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.factorial dpow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Nat.factorial_zero Nat.cast_one one_mul pow_zero dpow_zero Nat.factorial_succ mul_comm Nat.choose_one_right Nat.choose_symm_add Nat.cast_mul mul_assoc mul_dpow dpow_one pow_succ
mul_dpow 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib dpow AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.choose	—	—
nilpotent_of_mem_dpIdeal 📖	mathematical	AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	nsmul_eq_mul Nat.cast_mul Nat.mul_factorial_pred factorial_mul_dpow_eq_pow smul_mul_assoc IsScalarTower.right Ideal.mul_mem_left dpow_mem
ofRingEquiv_dpow 📖	mathematical	Ideal.map RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike	dpow ofRingEquiv DFunLike.coe RingEquiv.symm	—	—
ofRingEquiv_dpow_apply 📖	mathematical	Ideal.map RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike	dpow ofRingEquiv DFunLike.coe	—	RingEquiv.symm_apply_apply
prod_dpow 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Finset.prod CommSemiring.toCommMonoid dpow Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.multinomial Finset.sum Nat.instAddCommMonoid	—	Finset.induction Nat.multinomial_empty Nat.cast_one one_mul dpow_zero Finset.prod_insert mul_assoc mul_comm mul_dpow Finset.sum_insert Nat.multinomial_insert Nat.cast_mul

(root)

Definitions

Name	Category	Theorems
DividedPowers 📖	CompData	3 math math: DividedPowers.equiv_apply, DividedPowers.equiv_apply', DividedPowers.coe_injective
dividedPowersBot 📖	CompOp	1 math math: dividedPowersBot_dpow_eq
instCoeFunDividedPowersForallNatForall 📖	CompOp	—
instInhabitedDividedPowersBotIdeal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dividedPowersBot_dpow_eq 📖	mathematical	—	DividedPowers.dpow Bot.bot Ideal CommSemiring.toSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule dividedPowersBot MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—

---

← Back to Index