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_finsupp_sum, dpow_linearCombination, dpow_mem, dpow_mul, dpow_mul_right, dpow_null, dpow_one, dpow_prod, 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	32
Total	40

DividedPowers

Definitions

Name	Category	Theorems
dpow 📖	CompOp	54 math math: dpow_mem, RatAlgebra.dpow_eq_inv_fact_smul, factorial_mul_dpow_eq_pow, OfInvertibleFactorial.dpow_apply, Quotient.OfSurjective.dpow_def, SubDPIdeal.dpow_mem_span_of_mem_span, dpow_null, ext_iff, mem_dpEqualizer_iff, coincide_on_smul, ofRingEquiv_dpow, equiv_apply, dpow_comp_from_gens, dpow_comp, dpow_prod, 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, dpow_linearCombination, 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, dpow_finsupp_sum
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 NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid 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 NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid 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 NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring 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_finsupp_sum 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike	dpow Finsupp.sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Finset.sum Sym Finset.sym Finsupp.support Finsupp.prod CommSemiring.toCommMonoid Multiset.count Sym.toMultiset	—	Finset.sum_congr dpow_sum Finset.prod_congr
dpow_linearCombination 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	dpow Finsupp.sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toSMul Finset.sum Sym Finset.sym Finsupp.support Finsupp.prod CommSemiring.toCommMonoid Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Multiset.count Sym.toMultiset	—	Finsupp.sum.eq_1 dpow_sum Submodule.smul_of_tower_mem IsScalarTower.right Finset.sum_congr Finset.prod_congr Algebra.smul_def dpow_mul map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
dpow_mem 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	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 NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Monoid.toPow 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 NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Monoid.toPow 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 NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	—
dpow_one 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	dpow	—	—
dpow_prod 📖	mathematical	Finset.Nonempty Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	dpow Finset.prod CommSemiring.toCommMonoid AddMonoid.toNSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring Monoid.toPow Nat.instMonoid Nat.factorial Finset.card	—	Finset.induction Finset.prod_insert dpow_mul Finset.prod_eq_prod_diff_singleton_mul Ideal.mul_mem_left Finset.mem_insert_of_mem nsmul_eq_mul Nat.cast_pow Finset.card_insert_of_notMem add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid mul_comm pow_succ mul_assoc factorial_mul_dpow_eq_pow Finset.mem_insert_self Finset.prod_congr Finset.not_nonempty_iff_eq_empty mul_one Finset.instLawfulSingleton Finset.card_singleton tsub_self Nat.instCanonicallyOrderedAdd pow_zero Finset.prod_singleton one_smul
dpow_smul 📖	mathematical	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	dpow Algebra.toSMul CommSemiring.toSemiring Algebra.id Monoid.toPow 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 CommSemiring.toSemiring Algebra.id Monoid.toPow 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 NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring 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	Finset.sum Sym NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	—
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 EquivLike.toFunLike Equiv.instEquivLike equiv RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd RingEquiv.instEquivLike 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 EquivLike.toFunLike Equiv.instEquivLike equiv RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd RingEquiv.instEquivLike	—	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 NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring 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	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring 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 NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.factorial dpow Monoid.toPow 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 NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring dpow AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.choose	—	—
nilpotent_of_mem_dpIdeal 📖	mathematical	AddMonoid.toNSMul 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	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 Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike 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 Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike	—	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 NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring 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