Exp

📁 Source: Mathlib/RingTheory/PowerSeries/Exp.lean

Statistics

Metric	Count
Definitions exp	1
Theorems coeff_exp, constantCoeff_exp, derivative_exp, exp_mul_exp_eq_exp_add, exp_mul_exp_neg_eq_one, exp_pow_eq_rescale_exp, exp_pow_sum, exp_unique_of_derivative_eq_self, isUnit_exp, map_exp, order_exp	11
Total	12

PowerSeries

Definitions

Name	Category	Theorems
exp 📖	CompOp	14 math math: derivative_exp, exp_unique_of_derivative_eq_self, isUnit_exp, Polynomial.bernoulli_generating_function, bernoulliPowerSeries_mul_exp_sub_one, bernoulli'PowerSeries_mul_exp_sub_one, exp_mul_exp_neg_eq_one, exp_mul_exp_eq_exp_add, exp_pow_sum, coeff_exp, order_exp, exp_pow_eq_rescale_exp, constantCoeff_exp, map_exp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_exp 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff exp RingHom CommSemiring.toSemiring Rat.commSemiring RingHom.instFunLike algebraMap Nat.factorial	—	—
constantCoeff_exp 📖	mathematical	—	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring instSemiring Ring.toSemiring RingHom.instFunLike constantCoeff exp AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	coeff_zero_eq_constantCoeff_apply coeff_exp Nat.cast_one div_self NeZero.charZero_one Rat.instCharZero map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
derivative_exp 📖	mathematical	—	DFunLike.coe Derivation PowerSeries CommRing.toCommSemiring instCommSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instAlgebra Algebra.id Semiring.toModule instModule Derivation.instFunLike derivative exp CommRing.toRing	—	ext coeff_derivative coeff_exp map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_natCast map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Nat.factorial_succ Nat.cast_mul Nat.cast_add_one Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Rat.instAddLeftMono Nat.cast_nonneg' Rat.instZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Rat.instIsStrictOrderedRing Rat.nontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Nat.cast_pos' NeZero.charZero_one Rat.instCharZero Nat.factorial_pos one_ne_zero NeZero.one GroupWithZero.toNontrivial
exp_mul_exp_eq_exp_add 📖	mathematical	—	PowerSeries MvPowerSeries.instMul CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring instSemiring RingHom.instFunLike rescale exp CommRing.toRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	ext coeff_mul Finset.sum_congr add_pow Finset.sum_mul map_natCast RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.congr_arg mul_one_div one_div_mul_one_div div_eq_iff Nat.factorial_ne_zero Nat.cast_eq_zero Rat.instCharZero div_mul_eq_mul_div one_mul Nat.choose_eq_factorial_div_factorial Finset.mem_range_succ_iff Nat.cast_div_charZero Nat.factorial_mul_factorial_dvd_factorial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_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
exp_mul_exp_neg_eq_one 📖	mathematical	—	PowerSeries MvPowerSeries.instMul CommSemiring.toSemiring CommRing.toCommSemiring exp CommRing.toRing DFunLike.coe RingHom Semiring.toNonAssocSemiring instSemiring RingHom.instFunLike evalNegHom MvPowerSeries.instOne	—	rescale_one add_neg_cancel rescale_zero constantCoeff_exp map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass exp_mul_exp_eq_exp_add
exp_pow_eq_rescale_exp 📖	mathematical	—	PowerSeries Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring CommSemiring.toSemiring CommRing.toCommSemiring exp CommRing.toRing DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike rescale AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	pow_zero Nat.cast_zero rescale_zero constantCoeff_exp map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Nat.cast_add Nat.cast_one exp_mul_exp_eq_exp_add rescale_one pow_succ
exp_pow_sum 📖	mathematical	—	Finset.sum PowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring CommSemiring.toSemiring CommRing.toCommSemiring exp CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DFunLike.coe RingHom Semiring.toNonAssocSemiring Rat.commSemiring RingHom.instFunLike algebraMap Nat.factorial	—	Finset.sum_congr exp_pow_eq_rescale_exp ext coeff_exp one_div map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
exp_unique_of_derivative_eq_self 📖	mathematical	DFunLike.coe Derivation PowerSeries CommRing.toCommSemiring instCommSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instAlgebra Algebra.id Semiring.toModule instModule Derivation.instFunLike derivative RingHom instSemiring RingHom.instFunLike constantCoeff AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	exp	—	ext coeff_zero_eq_constantCoeff constantCoeff_exp derivative_exp coeff_derivative IsAddTorsionFree.to_isTorsionFree_nat Nat.instIsCancelMulZero nsmul_eq_mul mul_comm Nat.cast_succ
isUnit_exp 📖	mathematical	—	IsUnit PowerSeries MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring Ring.toSemiring exp	—	isUnit_iff_constantCoeff constantCoeff_exp
map_exp 📖	mathematical	—	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring instSemiring Ring.toSemiring RingHom.instFunLike map exp	—	ext coeff_exp one_div RingHom.map_rat_algebraMap
order_exp 📖	mathematical	—	order Ring.toSemiring exp ENat instZeroENat	—	order_zero_of_unit isUnit_exp

---

← Back to Index