Weierstrass

📁 Source: Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean

Statistics

Metric	Count
Definitions PeriodPair, G, basis, derivWeierstrassP, derivWeierstrassPExcept, derivWeierstrassPExceptSeries, g₂, g₃, lattice, latticeBasis, latticeEquivProd, sumInvPow, weierstrassP, weierstrassPExcept, weierstrassPExceptSeries, weierstrassPExceptSummand, weierstrassPSeries, weierstrassPSummand, «term℘'[_-_]», «term℘'[_]», «term℘[_-_]», «term℘[_]», ω₁, ω₂	24
Theorems G_eq_zero_of_odd, analyticAt_derivWeierstrassPExcept, analyticAt_weierstrassPExcept, analyticOnNhd_derivWeierstrassP, analyticOnNhd_derivWeierstrassPExcept, analyticOnNhd_weierstrassP, analyticOnNhd_weierstrassPExcept, basis_one, basis_zero, coeff_weierstrassPExceptSeries, coeff_weierstrassPSeries, compl_lattice_diff_singleton_mem_nhds, derivWeierstrassPExcept_add_coe, derivWeierstrassPExcept_def, derivWeierstrassPExcept_neg, derivWeierstrassPExcept_of_notMem, derivWeierstrassPExcept_sub, derivWeierstrassPExcept_zero_zero, derivWeierstrassP_add_coe, derivWeierstrassP_coe, derivWeierstrassP_neg, derivWeierstrassP_sq, derivWeierstrassP_sub_coe, derivWeierstrassP_zero, deriv_derivWeierstrassPExcept_self, deriv_weierstrassP, deriv_weierstrassPExcept_same, differentiableOn_derivWeierstrassP, differentiableOn_derivWeierstrassPExcept, differentiableOn_weierstrassP, differentiableOn_weierstrassPExcept, eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, finrank_lattice, hasFPowerSeriesAt_derivWeierstrassPExcept, hasFPowerSeriesAt_weierstrassPExcept, hasFPowerSeriesOnBall_derivWeierstrassPExcept, hasFPowerSeriesOnBall_weierstrassP, hasFPowerSeriesOnBall_weierstrassPExcept, hasSumLocallyUniformly_aux, hasSumLocallyUniformly_derivWeierstrassP, hasSumLocallyUniformly_derivWeierstrassPExcept, hasSumLocallyUniformly_weierstrassP, hasSumLocallyUniformly_weierstrassPExcept, hasSum_derivWeierstrassP, hasSum_derivWeierstrassPExcept, hasSum_sumInvPow, hasSum_weierstrassP, hasSum_weierstrassPExcept, indep, instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice, instIsZLatticeRealComplexLattice, instProperSpaceSubtypeComplexMemSubmoduleIntLattice, isClosed_lattice, isClosed_of_subset_lattice, isOpen_compl_lattice_diff, ite_eq_one_sub_sq_mul_weierstrassP, iteratedDeriv_derivWeierstrassPExcept_self, iteratedDeriv_weierstrassPExcept_self, latticeBasis_one, latticeBasis_zero, latticeEquiv_symm_apply, lattice_eq_span_range_basis, mem_lattice, meromorphic_derivWeierstrassP, meromorphic_weierstrassP, mul_ω₁_add_mul_ω₂_mem_lattice, not_continuousAt_weierstrassP, order_weierstrassP, periodic_derivWeierstrassP, periodic_weierstrassP, sumInvPow_zero, summable_weierstrassPExceptSummand, summable_weierstrassPSummand, weierstrassPExceptSeries_hasSum, weierstrassPExceptSeries_of_notMem, weierstrassPExceptSummand_of_notMem, weierstrassPExcept_add, weierstrassPExcept_def, weierstrassPExcept_eq_tsum, weierstrassPExcept_neg, weierstrassPExcept_of_notMem, weierstrassPExcept_zero, weierstrassPSeries_hasSum, weierstrassP_add_coe, weierstrassP_bound, weierstrassP_coe, weierstrassP_neg, weierstrassP_sub_coe, weierstrassP_zero, ω₁_div_two_notMem_lattice, ω₁_mem_lattice, ω₂_div_two_notMem_lattice, ω₂_mem_lattice	93
Total	117

PeriodPair

Definitions

Name	Category	Theorems
G 📖	CompOp	2 math math: G_eq_zero_of_odd, sumInvPow_zero
basis 📖	CompOp	3 math math: basis_one, basis_zero, lattice_eq_span_range_basis
derivWeierstrassP 📖	CompOp	16 math math: deriv_weierstrassP, derivWeierstrassPExcept_sub, derivWeierstrassP_neg, hasSum_derivWeierstrassP, hasSumLocallyUniformly_derivWeierstrassP, derivWeierstrassPExcept_of_notMem, periodic_derivWeierstrassP, differentiableOn_derivWeierstrassP, meromorphic_derivWeierstrassP, derivWeierstrassP_sq, derivWeierstrassP_sub_coe, derivWeierstrassP_coe, analyticOnNhd_derivWeierstrassP, derivWeierstrassPExcept_def, derivWeierstrassP_add_coe, derivWeierstrassP_zero
derivWeierstrassPExcept 📖	CompOp	17 math math: derivWeierstrassPExcept_sub, iteratedDeriv_derivWeierstrassPExcept_self, eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, hasSum_derivWeierstrassPExcept, hasFPowerSeriesAt_derivWeierstrassPExcept, analyticOnNhd_derivWeierstrassPExcept, derivWeierstrassPExcept_of_notMem, hasSumLocallyUniformly_derivWeierstrassPExcept, deriv_derivWeierstrassPExcept_self, hasFPowerSeriesOnBall_derivWeierstrassPExcept, deriv_weierstrassPExcept_same, analyticAt_derivWeierstrassPExcept, derivWeierstrassPExcept_neg, derivWeierstrassPExcept_add_coe, derivWeierstrassPExcept_zero_zero, derivWeierstrassPExcept_def, differentiableOn_derivWeierstrassPExcept
derivWeierstrassPExceptSeries 📖	CompOp	1 math math: hasFPowerSeriesOnBall_derivWeierstrassPExcept
g₂ 📖	CompOp	1 math math: derivWeierstrassP_sq
g₃ 📖	CompOp	1 math math: derivWeierstrassP_sq
lattice 📖	CompOp	50 math math: hasSumLocallyUniformly_weierstrassP, coeff_weierstrassPExceptSeries, derivWeierstrassPExcept_sub, ω₁_div_two_notMem_lattice, eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, weierstrassP_coe, hasSum_derivWeierstrassPExcept, latticeBasis_zero, ω₂_div_two_notMem_lattice, hasSum_derivWeierstrassP, compl_lattice_diff_singleton_mem_nhds, hasSumLocallyUniformly_derivWeierstrassP, mem_lattice, analyticOnNhd_derivWeierstrassPExcept, isClosed_lattice, periodic_derivWeierstrassP, differentiableOn_derivWeierstrassP, weierstrassPExcept_def, hasSumLocallyUniformly_weierstrassPExcept, derivWeierstrassP_sub_coe, weierstrassP_add_coe, instProperSpaceSubtypeComplexMemSubmoduleIntLattice, latticeBasis_one, weierstrassP_sub_coe, hasSum_weierstrassP, coeff_weierstrassPSeries, isOpen_compl_lattice_diff, derivWeierstrassP_coe, latticeEquiv_symm_apply, hasSumLocallyUniformly_derivWeierstrassPExcept, analyticOnNhd_derivWeierstrassP, instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice, hasSum_weierstrassPExcept, differentiableOn_weierstrassPExcept, derivWeierstrassPExcept_add_coe, differentiableOn_weierstrassP, hasSum_sumInvPow, periodic_weierstrassP, mul_ω₁_add_mul_ω₂_mem_lattice, analyticOnNhd_weierstrassPExcept, lattice_eq_span_range_basis, ω₁_mem_lattice, analyticOnNhd_weierstrassP, ω₂_mem_lattice, derivWeierstrassPExcept_def, finrank_lattice, derivWeierstrassP_add_coe, weierstrassPExcept_add, instIsZLatticeRealComplexLattice, differentiableOn_derivWeierstrassPExcept
latticeBasis 📖	CompOp	2 math math: latticeBasis_zero, latticeBasis_one
latticeEquivProd 📖	CompOp	1 math math: latticeEquiv_symm_apply
sumInvPow 📖	CompOp	7 math math: hasFPowerSeriesAt_weierstrassPExcept, iteratedDeriv_weierstrassPExcept_self, iteratedDeriv_derivWeierstrassPExcept_self, hasFPowerSeriesAt_derivWeierstrassPExcept, sumInvPow_zero, deriv_derivWeierstrassPExcept_self, hasSum_sumInvPow
weierstrassP 📖	CompOp	21 math math: hasSumLocallyUniformly_weierstrassP, deriv_weierstrassP, weierstrassP_coe, weierstrassP_zero, ite_eq_one_sub_sq_mul_weierstrassP, weierstrassPExcept_def, derivWeierstrassP_sq, weierstrassP_add_coe, order_weierstrassP, weierstrassP_sub_coe, hasSum_weierstrassP, hasFPowerSeriesOnBall_weierstrassP, weierstrassPSeries_hasSum, meromorphic_weierstrassP, not_continuousAt_weierstrassP, differentiableOn_weierstrassP, periodic_weierstrassP, weierstrassP_neg, weierstrassPExcept_of_notMem, analyticOnNhd_weierstrassP, weierstrassPExcept_add
weierstrassPExcept 📖	CompOp	18 math math: hasFPowerSeriesAt_weierstrassPExcept, iteratedDeriv_weierstrassPExcept_self, eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, analyticAt_weierstrassPExcept, ite_eq_one_sub_sq_mul_weierstrassP, weierstrassPExcept_neg, weierstrassPExcept_eq_tsum, weierstrassPExcept_def, weierstrassPExcept_zero, hasSumLocallyUniformly_weierstrassPExcept, deriv_weierstrassPExcept_same, hasFPowerSeriesOnBall_weierstrassPExcept, hasSum_weierstrassPExcept, differentiableOn_weierstrassPExcept, weierstrassPExceptSeries_hasSum, analyticOnNhd_weierstrassPExcept, weierstrassPExcept_of_notMem, weierstrassPExcept_add
weierstrassPExceptSeries 📖	CompOp	5 math math: coeff_weierstrassPExceptSeries, weierstrassPExcept_eq_tsum, weierstrassPExceptSeries_of_notMem, hasFPowerSeriesOnBall_weierstrassPExcept, weierstrassPExceptSeries_hasSum
weierstrassPExceptSummand 📖	CompOp	3 math math: coeff_weierstrassPExceptSeries, weierstrassPExceptSummand_of_notMem, summable_weierstrassPExceptSummand
weierstrassPSeries 📖	CompOp	4 math math: weierstrassPExceptSeries_of_notMem, coeff_weierstrassPSeries, hasFPowerSeriesOnBall_weierstrassP, weierstrassPSeries_hasSum
weierstrassPSummand 📖	CompOp	3 math math: weierstrassPExceptSummand_of_notMem, summable_weierstrassPSummand, coeff_weierstrassPSeries
«term℘'[_-_]» 📖	CompOp	—
«term℘'[_]» 📖	CompOp	—
«term℘[_-_]» 📖	CompOp	—
«term℘[_]» 📖	CompOp	—
ω₁ 📖	CompOp	8 math math: ω₁_div_two_notMem_lattice, latticeBasis_zero, mem_lattice, basis_zero, latticeEquiv_symm_apply, mul_ω₁_add_mul_ω₂_mem_lattice, indep, ω₁_mem_lattice
ω₂ 📖	CompOp	8 math math: basis_one, ω₂_div_two_notMem_lattice, mem_lattice, latticeBasis_one, latticeEquiv_symm_apply, mul_ω₁_add_mul_ω₂_mem_lattice, indep, ω₂_mem_lattice

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
G_eq_zero_of_odd 📖	mathematical	Odd Nat.instSemiring	G Complex Complex.instZero	—	CharZero.eq_neg_self_iff NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Complex.instCharZero G.eq_1 tsum_neg SeminormedAddCommGroup.toIsTopologicalAddGroup Complex.instT2Space Equiv.tsum_eq Odd.neg_pow neg_inv
analyticAt_derivWeierstrassPExcept 📖	mathematical	—	AnalyticAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace derivWeierstrassPExcept	—	analyticOnNhd_derivWeierstrassPExcept
analyticAt_weierstrassPExcept 📖	mathematical	—	AnalyticAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace weierstrassPExcept	—	analyticOnNhd_weierstrassPExcept
analyticOnNhd_derivWeierstrassP 📖	mathematical	—	AnalyticOnNhd Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace derivWeierstrassP Compl.compl Set Set.instCompl SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule Complex.addCommGroup Submodule.setLike lattice	—	DifferentiableOn.analyticOnNhd Complex.instCompleteSpace differentiableOn_derivWeierstrassP IsClosed.isOpen_compl isClosed_lattice
analyticOnNhd_derivWeierstrassPExcept 📖	mathematical	—	AnalyticOnNhd Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace derivWeierstrassPExcept Compl.compl Set Set.instCompl Set.instSDiff SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule Complex.addCommGroup Submodule.setLike lattice Set.instSingletonSet	—	DifferentiableOn.analyticOnNhd Complex.instCompleteSpace differentiableOn_derivWeierstrassPExcept isOpen_compl_lattice_diff
analyticOnNhd_weierstrassP 📖	mathematical	—	AnalyticOnNhd Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace weierstrassP Compl.compl Set Set.instCompl SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule Complex.addCommGroup Submodule.setLike lattice	—	DifferentiableOn.analyticOnNhd Complex.instCompleteSpace differentiableOn_weierstrassP IsClosed.isOpen_compl isClosed_lattice
analyticOnNhd_weierstrassPExcept 📖	mathematical	—	AnalyticOnNhd Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace weierstrassPExcept Compl.compl Set Set.instCompl Set.instSDiff SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule Complex.addCommGroup Submodule.setLike lattice Set.instSingletonSet	—	DifferentiableOn.analyticOnNhd Complex.instCompleteSpace differentiableOn_weierstrassPExcept isOpen_compl_lattice_diff
basis_one 📖	mathematical	—	DFunLike.coe Module.Basis Real Complex Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex Module.Basis.instFunLike basis ω₂	—	indep coe_basisOfLinearIndependentOfCardEqFinrank Matrix.cons_val_fin_one
basis_zero 📖	mathematical	—	DFunLike.coe Module.Basis Real Complex Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex Module.Basis.instFunLike basis ω₁	—	indep coe_basisOfLinearIndependentOfCardEqFinrank
coeff_weierstrassPExceptSeries 📖	mathematical	—	FormalMultilinearSeries.coeff Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace weierstrassPExceptSeries tsum Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice weierstrassPExceptSummand SummationFilter.unconditional	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul sub_sq_comm one_div FormalMultilinearSeries.coeff_ofScalars CharP.cast_eq_zero CharP.ofCharZero Complex.instCharZero zero_add Nat.instAtLeastTwoHAddOfNat zpow_neg zpow_ofNat one_mul IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing tsum_ite_eq SummationFilter.instLeAtTopUnconditional zpow_natCast Nat.cast_add Nat.cast_one add_assoc one_add_one_eq_two sumInvPow.eq_1 Summable.tsum_sub SeminormedAddCommGroup.toIsTopologicalAddGroup Complex.instT2Space SummationFilter.instNeBotUnconditional HasSum.summable hasSum_sumInvPow lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl 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.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt 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.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_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 Mathlib.Tactic.Linarith.natCast_nonneg summable_of_finite_support SummationFilter.instHasSupportOfLeAtTop Set.Finite.subset Set.finite_singleton neg_add_rev tsum_mul_left sub_self MulZeroClass.mul_zero Nat.cast_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.pow_congr 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_bit1 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.pow_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.atom_pf' sub_zero
coeff_weierstrassPSeries 📖	mathematical	—	FormalMultilinearSeries.coeff Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace weierstrassPSeries tsum Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice weierstrassPSummand SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul weierstrassPExceptSeries_of_notMem ω₁_div_two_notMem_lattice coeff_weierstrassPExceptSeries weierstrassPExceptSummand_of_notMem
compl_lattice_diff_singleton_mem_nhds 📖	mathematical	—	Set Complex Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Compl.compl Set.instCompl Set.instSDiff SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup Submodule.setLike lattice Set.instSingletonSet	—	IsOpen.mem_nhds isOpen_compl_lattice_diff
derivWeierstrassPExcept_add_coe 📖	mathematical	—	derivWeierstrassPExcept Complex Complex.instAdd Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Complex.instSub	—	Equiv.tsum_eq add_sub_add_right_eq_sub
derivWeierstrassPExcept_def 📖	mathematical	—	derivWeierstrassPExcept Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Complex.instAdd derivWeierstrassP DivInvMonoid.toDiv Complex.instDivInvMonoid instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instSub	—	Nat.instAtLeastTwoHAddOfNat derivWeierstrassPExcept_sub sub_add_cancel
derivWeierstrassPExcept_neg 📖	mathematical	—	derivWeierstrassPExcept Complex Complex.instNeg	—	Equiv.tsum_eq sub_neg_eq_add neg_add_eq_sub SeminormedAddCommGroup.toIsTopologicalAddGroup Complex.instT2Space neg_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.pow_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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_bit1 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.atom_pf'
derivWeierstrassPExcept_of_notMem 📖	mathematical	Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	derivWeierstrassPExcept derivWeierstrassP	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Complex.instT2Space neg_div
derivWeierstrassPExcept_sub 📖	mathematical	—	Complex Complex.instSub derivWeierstrassPExcept Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice DivInvMonoid.toDiv Complex.instDivInvMonoid instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring derivWeierstrassP	—	Nat.instAtLeastTwoHAddOfNat sub_eq_add_neg neg_div tsum_ite_eq SummationFilter.instLeAtTopUnconditional derivWeierstrassP.eq_1 derivWeierstrassPExcept.eq_1 Summable.tsum_add Complex.instT2Space IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SummationFilter.instNeBotUnconditional hasSum_derivWeierstrassPExcept summable_of_finite_support SummationFilter.instHasSupportOfLeAtTop Set.Finite.subset Set.finite_singleton Complex.instCharZero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero tsum_neg SeminormedAddCommGroup.toIsTopologicalAddGroup zero_add add_zero
derivWeierstrassPExcept_zero_zero 📖	mathematical	—	derivWeierstrassPExcept Complex Complex.instZero	—	neg_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Complex.instCharZero derivWeierstrassPExcept_neg
derivWeierstrassP_add_coe 📖	mathematical	—	derivWeierstrassP Complex Complex.instAdd Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	—	Equiv.tsum_eq add_sub_add_right_eq_sub SeminormedAddCommGroup.toIsTopologicalAddGroup Complex.instT2Space
derivWeierstrassP_coe 📖	mathematical	—	derivWeierstrassP Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Complex.instZero	—	zero_add derivWeierstrassP_add_coe derivWeierstrassP_zero
derivWeierstrassP_neg 📖	mathematical	—	derivWeierstrassP Complex Complex.instNeg	—	Equiv.tsum_eq sub_neg_eq_add neg_add_eq_sub SeminormedAddCommGroup.toIsTopologicalAddGroup Complex.instT2Space neg_neg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf 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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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_bit1 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_zero
derivWeierstrassP_sq 📖	mathematical	Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring derivWeierstrassP Complex.instSub Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat weierstrassP g₂ g₃	—	sub_add
derivWeierstrassP_sub_coe 📖	mathematical	—	derivWeierstrassP Complex Complex.instSub Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	—	derivWeierstrassP_add_coe sub_add_cancel
derivWeierstrassP_zero 📖	mathematical	—	derivWeierstrassP Complex Complex.instZero	—	CharZero.eq_neg_self_iff NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Complex.instCharZero derivWeierstrassP_neg neg_zero
deriv_derivWeierstrassPExcept_self 📖	mathematical	—	deriv Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField derivWeierstrassPExcept Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat sumInvPow	—	iteratedDeriv_one iteratedDeriv_derivWeierstrassPExcept_self
deriv_weierstrassP 📖	mathematical	—	deriv Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField weierstrassP derivWeierstrassP	—	deriv_zero_of_not_differentiableAt not_continuousAt_weierstrassP DifferentiableAt.continuousAt IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology derivWeierstrassP_coe Nat.instAtLeastTwoHAddOfNat weierstrassPExcept_of_notMem ω₁_div_two_notMem_lattice derivWeierstrassPExcept_of_notMem eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept
deriv_weierstrassPExcept_same 📖	mathematical	—	deriv Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField weierstrassPExcept derivWeierstrassPExcept	—	eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept
differentiableOn_derivWeierstrassP 📖	mathematical	—	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField derivWeierstrassP Compl.compl Set Set.instCompl SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Submodule.setLike lattice	—	Nat.instAtLeastTwoHAddOfNat derivWeierstrassPExcept_of_notMem ω₁_div_two_notMem_lattice Set.diff_singleton_eq_self differentiableOn_derivWeierstrassPExcept
differentiableOn_derivWeierstrassPExcept 📖	mathematical	—	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField derivWeierstrassPExcept Compl.compl Set Set.instCompl Set.instSDiff SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Submodule.setLike lattice Set.instSingletonSet	—	TendstoLocallyUniformlyOn.differentiableOn Nat.instAtLeastTwoHAddOfNat Complex.instCompleteSpace Filter.atTop_neBot Finset.isDirected_le TendstoLocallyUniformly.tendstoLocallyUniformlyOn hasSumLocallyUniformly_derivWeierstrassPExcept Filter.Eventually.of_forall DifferentiableOn.fun_sum DifferentiableOn.div differentiableOn_const DifferentiableOn.fun_pow DifferentiableOn.sub_const differentiableOn_id isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero isOpen_compl_lattice_diff
differentiableOn_weierstrassP 📖	mathematical	—	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField weierstrassP Compl.compl Set Set.instCompl SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Submodule.setLike lattice	—	Nat.instAtLeastTwoHAddOfNat weierstrassPExcept_of_notMem ω₁_div_two_notMem_lattice Set.diff_singleton_eq_self differentiableOn_weierstrassPExcept
differentiableOn_weierstrassPExcept 📖	mathematical	—	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField weierstrassPExcept Compl.compl Set Set.instCompl Set.instSDiff SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Submodule.setLike lattice Set.instSingletonSet	—	TendstoLocallyUniformlyOn.differentiableOn Complex.instCompleteSpace Filter.atTop_neBot Finset.isDirected_le HasSumLocallyUniformly.hasSumLocallyUniformlyOn hasSumLocallyUniformly_weierstrassPExcept Filter.Eventually.of_forall DifferentiableOn.fun_sum DifferentiableOn.sub DifferentiableOn.div differentiableOn_const DifferentiableOn.fun_pow DifferentiableOn.sub_const differentiableOn_id isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat isOpen_compl_lattice_diff
eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept 📖	mathematical	—	Set.EqOn Complex deriv DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField weierstrassPExcept derivWeierstrassPExcept Compl.compl Set Set.instCompl Set.instSDiff SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Submodule.setLike lattice Set.instSingletonSet	—	TendstoLocallyUniformlyOn.unique Filter.atTop_neBot Finset.isDirected_le Complex.instT2Space TendstoLocallyUniformlyOn.deriv Complex.instCompleteSpace TendstoLocallyUniformly.tendstoLocallyUniformlyOn hasSumLocallyUniformly_weierstrassPExcept Filter.Eventually.of_forall DifferentiableOn.fun_sum DifferentiableOn.sub DifferentiableOn.div differentiableOn_const DifferentiableOn.fun_pow DifferentiableOn.sub_const differentiableOn_id isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat isOpen_compl_lattice_diff TendstoLocallyUniformlyOn.congr hasSumLocallyUniformly_derivWeierstrassPExcept Finset.sum_congr deriv_fun_sum sub_eq_zero DifferentiableAt.sub DifferentiableAt.div differentiableAt_const DifferentiableAt.fun_pow DifferentiableAt.sub_const differentiableAt_id deriv_const' deriv_fun_sub DifferentiableAt.fun_div deriv_const one_div deriv_comp_sub_const deriv_zpow Int.cast_neg Int.cast_ofNat zpow_neg neg_mul sub_zero Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul neg_div Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.zpow_eq_eval Mathlib.Tactic.FieldSimp.subst_sub 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.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval mul_neg Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Mathlib.Meta.NormNum.isNat_eq_false Complex.instCharZero Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial
finrank_lattice 📖	mathematical	—	Module.finrank Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Submodule.addCommMonoid Submodule.addCommGroup Int.instRing	—	Module.finrank_eq_card_basis commRing_strongRankCondition Int.instNontrivial
hasFPowerSeriesAt_derivWeierstrassPExcept 📖	mathematical	—	HasFPowerSeriesAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace derivWeierstrassPExcept FormalMultilinearSeries.ofScalars Complex.instField Complex.instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instMul Complex.instAdd Complex.instNatCast Complex.instOne instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat sumInvPow	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Nat.instAtLeastTwoHAddOfNat Filter.HasBasis.mem_iff Metric.nhds_basis_closedBall compl_lattice_diff_singleton_mem_nhds IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul SMulCommClass.continuousConstSMul Algebra.to_smulCommClass sub_self zero_pow Nat.instCharZero inv_zero sub_zero HasFPowerSeriesOnBall.hasFPowerSeriesAt LT.lt.le hasFPowerSeriesOnBall_derivWeierstrassPExcept
hasFPowerSeriesAt_weierstrassPExcept 📖	mathematical	—	HasFPowerSeriesAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace weierstrassPExcept FormalMultilinearSeries.ofScalars Complex.instField Complex.instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instMul Complex.instAdd Complex.instNatCast Complex.instOne sumInvPow	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Filter.HasBasis.mem_iff Metric.nhds_basis_closedBall compl_lattice_diff_singleton_mem_nhds CanLift.prf NNReal.canLift LT.lt.le IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul SMulCommClass.continuousConstSMul Algebra.to_smulCommClass sub_self zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat inv_zero sub_zero HasFPowerSeriesOnBall.hasFPowerSeriesAt hasFPowerSeriesOnBall_weierstrassPExcept
hasFPowerSeriesOnBall_derivWeierstrassPExcept 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal Set Complex Set.instHasSubset Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NNReal.toReal Compl.compl Set.instCompl Set.instSDiff SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup Submodule.setLike lattice Set.instSingletonSet	HasFPowerSeriesOnBall DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace derivWeierstrassPExcept derivWeierstrassPExceptSeries ENNReal.ofNNReal	—	HasFPowerSeriesOnBall.congr RingHomIsometric.ids smulCommClass_self HasFPowerSeriesOnBall.fderiv Complex.instCompleteSpace hasFPowerSeriesOnBall_weierstrassPExcept Algebra.to_smulCommClass SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul FormalMultilinearSeries.ext IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul ContinuousMultilinearMap.ext_ring Finite.of_fintype FormalMultilinearSeries.apply_eq_prod_smul_coeff Finset.prod_const_one FormalMultilinearSeries.coeff_ofScalars one_mul ContinuousLinearMap.compContinuousMultilinearMap_coe one_smul FormalMultilinearSeries.derivSeries_coeff_one Nat.cast_add Nat.cast_one nsmul_eq_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero 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.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.sub_congr 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.isInt_add ContinuousLinearMap.comp_hasFPowerSeriesOnBall Set.EqOn.mono HasSubset.Subset.trans Set.instIsTransSubset Metric.eball_coe Metric.ball_subset_closedBall eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept
hasFPowerSeriesOnBall_weierstrassP 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal Set Complex Set.instHasSubset Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NNReal.toReal Compl.compl Set.instCompl SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup Submodule.setLike lattice	HasFPowerSeriesOnBall DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace weierstrassP weierstrassPSeries ENNReal.ofNNReal	—	Nat.instAtLeastTwoHAddOfNat IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul weierstrassPExceptSeries_of_notMem ω₁_div_two_notMem_lattice IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul weierstrassPExcept_of_notMem hasFPowerSeriesOnBall_weierstrassPExcept HasSubset.Subset.trans Set.instIsTransSubset Set.compl_subset_compl Set.diff_subset
hasFPowerSeriesOnBall_weierstrassPExcept 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal Set Complex Set.instHasSubset Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NNReal.toReal Compl.compl Set.instCompl Set.instSDiff SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup Submodule.setLike lattice Set.instSingletonSet	HasFPowerSeriesOnBall DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace weierstrassPExcept weierstrassPExceptSeries ENNReal.ofNNReal	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul FormalMultilinearSeries.le_radius_of_tendsto FormalMultilinearSeries.norm_apply_eq_norm_coef add_sub_cancel_left Complex.norm_mul norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass Complex.norm_real NNReal.abs_eq norm_zero Filter.Tendsto.comp tendsto_norm Summable.tendsto_atTop_zero HasSum.summable weierstrassPExceptSeries_hasSum Set.subset_compl_comm ENNReal.coe_pos Metric.eball_coe dist_zero_right IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul weierstrassPExceptSeries.eq_1 FormalMultilinearSeries.ofScalars_apply_eq FormalMultilinearSeries.coeff_ofScalars smul_eq_mul LT.lt.trans
hasSumLocallyUniformly_aux 📖	mathematical	Summable Real Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Real.instAddCommMonoid Real.pseudoMetricSpace SummationFilter.unconditional Filter.Eventually Filter.atTop Real.instPreorder	HasSumLocallyUniformly tsum	—	hasSumLocallyUniformly_iff_tendstoLocallyUniformly tendstoLocallyUniformly_iff_filter Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid norm_nonneg Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Filter.le_principal_iff IsOpen.mem_nhds Metric.isOpen_ball dist_zero_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike TendstoUniformlyOnFilter.mono_right tendstoUniformlyOn_iff_tendstoUniformlyOnFilter tendstoUniformlyOn_tsum_of_cofinite_eventually Complex.instCompleteSpace Filter.eventually_atTop instIsDirectedOrder Real.instArchimedean Set.Finite.subset isCompact_iff_finite instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice ProperSpace.isCompact_closedBall instProperSpaceSubtypeComplexMemSubmoduleIntLattice Mathlib.Tactic.Contrapose.contrapose₁ LT.lt.le
hasSumLocallyUniformly_derivWeierstrassP 📖	mathematical	—	HasSumLocallyUniformly Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instSub derivWeierstrassP	—	Nat.instAtLeastTwoHAddOfNat ω₁_div_two_notMem_lattice neg_div derivWeierstrassPExcept_of_notMem hasSumLocallyUniformly_derivWeierstrassPExcept
hasSumLocallyUniformly_derivWeierstrassPExcept 📖	mathematical	—	HasSumLocallyUniformly Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Complex.instDecidableEq Complex.instZero DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instSub derivWeierstrassPExcept	—	hasSumLocallyUniformly_aux Nat.instAtLeastTwoHAddOfNat Summable.mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ZLattice.summable_norm_rpow Complex.instFiniteDimensionalReal instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice finrank_lattice IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Mathlib.Meta.NormNum.isNat_lt_true Real.instIsOrderedRing RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Filter.eventually_atTop instIsDirectedOrder Real.instArchimedean norm_zero Real.rpow_neg_ofNat zpow_neg IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instNontrivial PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE pow_nonneg IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono norm_nonneg Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.atom_pf 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_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos 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_lt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.mul_neg Complex.norm_div norm_neg Complex.norm_ofNat norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass Real.rpow_neg div_eq_mul_inv div_le_div_iff₀ pow_pos Real.instZeroLEOneClass Real.rpow_pos_of_pos AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass norm_sub_rev LE.le.trans_eq Real.rpow_natCast mul_le_mul_of_nonneg_left pow_le_pow_left₀ IsOrderedRing.toMulPosMono le_of_lt norm_pos_iff le_trans le_of_not_gt mul_le_mul le_rfl norm_sub_norm_le Mathlib.Tactic.Ring.neg_congr Nat.cast_one neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit1 Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.one_pow
hasSumLocallyUniformly_weierstrassP 📖	mathematical	—	HasSumLocallyUniformly Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Complex.instSub DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring weierstrassP	—	Nat.instAtLeastTwoHAddOfNat ω₁_div_two_notMem_lattice weierstrassPExcept_of_notMem hasSumLocallyUniformly_weierstrassPExcept
hasSumLocallyUniformly_weierstrassPExcept 📖	mathematical	—	HasSumLocallyUniformly Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Complex.instDecidableEq Complex.instZero Complex.instSub DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring weierstrassPExcept	—	hasSumLocallyUniformly_aux Nat.instAtLeastTwoHAddOfNat Summable.mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ZLattice.summable_norm_rpow Complex.instFiniteDimensionalReal instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice finrank_lattice IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Mathlib.Meta.NormNum.isNat_lt_true Real.instIsOrderedRing RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Filter.eventually_atTop instIsDirectedOrder Real.instArchimedean norm_zero Real.rpow_neg_ofNat zpow_neg mul_nonneg IsOrderedRing.toPosMulMono le_of_lt mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial inv_nonneg_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE pow_nonneg IsOrderedRing.toZeroLEOneClass norm_nonneg weierstrassP_bound
hasSum_derivWeierstrassP 📖	mathematical	—	HasSum Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instSub derivWeierstrassP SummationFilter.unconditional	—	TendstoLocallyUniformlyOn.tendsto_at Nat.instAtLeastTwoHAddOfNat TendstoLocallyUniformly.tendstoLocallyUniformlyOn hasSumLocallyUniformly_derivWeierstrassP Set.mem_univ
hasSum_derivWeierstrassPExcept 📖	mathematical	—	HasSum Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Complex.instDecidableEq Complex.instZero DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instSub derivWeierstrassPExcept SummationFilter.unconditional	—	TendstoLocallyUniformlyOn.tendsto_at Nat.instAtLeastTwoHAddOfNat TendstoLocallyUniformly.tendstoLocallyUniformlyOn hasSumLocallyUniformly_derivWeierstrassPExcept Set.mem_univ
hasSum_sumInvPow 📖	mathematical	—	HasSum Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Complex.instInv Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instSub sumInvPow SummationFilter.unconditional	—	Summable.hasSum Summable.of_norm_bounded Complex.instCompleteSpace ZLattice.summable_norm_sub_zpow Complex.instFiniteDimensionalReal instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice Nat.instAtLeastTwoHAddOfNat finrank_lattice IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Int.instZeroLEOneClass Int.instCharZero zpow_natCast zpow_neg norm_zpow le_refl
hasSum_weierstrassP 📖	mathematical	—	HasSum Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Complex.instSub DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring weierstrassP SummationFilter.unconditional	—	HasSumLocallyUniformly.hasSum hasSumLocallyUniformly_weierstrassP
hasSum_weierstrassPExcept 📖	mathematical	—	HasSum Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Complex.instDecidableEq Complex.instZero Complex.instSub DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring weierstrassPExcept SummationFilter.unconditional	—	HasSumLocallyUniformly.hasSum hasSumLocallyUniformly_weierstrassPExcept
indep 📖	mathematical	—	LinearIndependent Real Complex Matrix.vecCons ω₁ ω₂ Matrix.vecEmpty Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex	—	—
instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice 📖	mathematical	—	DiscreteTopology Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice instTopologicalSpaceSubtype	—	ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite Finite.of_fintype lattice_eq_span_range_basis
instIsZLatticeRealComplexLattice 📖	mathematical	—	IsZLattice Real Real.normedField Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex lattice instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice	—	instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice lattice_eq_span_range_basis IsZLattice.congr_simp instIsZLatticeRealSpan Finite.of_fintype
instProperSpaceSubtypeComplexMemSubmoduleIntLattice 📖	mathematical	—	ProperSpace Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Subtype.pseudoMetricSpace	—	ProperSpace.of_isClosed Complex.instProperSpace isClosed_lattice
isClosed_lattice 📖	mathematical	—	IsClosed Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup Submodule.setLike lattice	—	AddSubgroup.isClosed_of_discrete SeminormedAddCommGroup.toIsTopologicalAddGroup Complex.instT2Space instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice
isClosed_of_subset_lattice 📖	mathematical	Set Complex Set.instHasSubset SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup Submodule.setLike lattice	IsClosed	—	Subtype.range_coe_subtype Set.image_preimage_eq_inter_range IsClosed.isClosedMap_subtype_val isClosed_lattice isClosed_discrete instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice
isOpen_compl_lattice_diff 📖	mathematical	—	IsOpen Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Compl.compl Set Set.instCompl Set.instSDiff SetLike.coe Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup Submodule.setLike lattice	—	IsClosed.isOpen_compl isClosed_of_subset_lattice Set.diff_subset
ite_eq_one_sub_sq_mul_weierstrassP 📖	mathematical	Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	Complex.instDecidableEq Complex.instOne Complex.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instSub weierstrassP Complex.instAdd weierstrassPExcept DivInvMonoid.toDiv Complex.instDivInvMonoid	—	—
iteratedDeriv_derivWeierstrassPExcept_self 📖	mathematical	—	iteratedDeriv Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace derivWeierstrassPExcept Complex.instMul Complex.instNatCast Nat.factorial sumInvPow	—	Nat.instAtLeastTwoHAddOfNat IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing FormalMultilinearSeries.coeff_ofScalars IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul HasFPowerSeriesAt.eq_formalMultilinearSeries AnalyticAt.hasFPowerSeriesAt Complex.instCompleteSpace Complex.instCharZero analyticAt_derivWeierstrassPExcept hasFPowerSeriesAt_derivWeierstrassPExcept Nat.cast_mul Nat.cast_add Nat.cast_one
iteratedDeriv_weierstrassPExcept_self 📖	mathematical	—	iteratedDeriv Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace weierstrassPExcept Complex.instMul Complex.instNatCast Nat.factorial sumInvPow	—	div_mul_cancel₀ Complex.instCharZero eq_div_iff_mul_eq IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing FormalMultilinearSeries.coeff_ofScalars IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul HasFPowerSeriesAt.eq_formalMultilinearSeries AnalyticAt.hasFPowerSeriesAt Complex.instCompleteSpace analyticAt_weierstrassPExcept hasFPowerSeriesAt_weierstrassPExcept Nat.cast_one div_one Nat.cast_add Nat.cast_mul 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.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 Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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.Meta.NormNum.IsNat.of_raw 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.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.zero_mul
latticeBasis_one 📖	mathematical	—	Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice DFunLike.coe Module.Basis Submodule.addCommMonoid Submodule.addCommGroup Int.instRing Module.Basis.instFunLike latticeBasis ω₂	—	Module.Basis.span_apply Matrix.cons_val_fin_one
latticeBasis_zero 📖	mathematical	—	Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice DFunLike.coe Module.Basis Submodule.addCommMonoid Submodule.addCommGroup Int.instRing Module.Basis.instFunLike latticeBasis ω₁	—	Module.Basis.span_apply
latticeEquiv_symm_apply 📖	mathematical	—	Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Prod.instAddCommMonoid Int.instAddCommMonoid Submodule.addCommMonoid Prod.instAddCommGroup Int.instAddCommGroup Submodule.addCommGroup Int.instRing EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm latticeEquivProd Complex.instAdd Complex.instMul Complex.instIntCast ω₁ ω₂	—	RingHomInvPair.ids Module.Basis.repr_symm_apply Finsupp.sum_zsmul Finset.sum_congr Fin.sum_univ_two Matrix.cons_val_fin_one latticeBasis_zero zsmul_eq_mul latticeBasis_one
lattice_eq_span_range_basis 📖	mathematical	—	lattice Submodule.span Complex Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup Set.range DFunLike.coe Module.Basis Real Real.semiring NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex Module.Basis.instFunLike basis	—	lattice.eq_1 Set.image_univ Finset.coe_univ Finset.coe_insert Finset.coe_singleton Set.image_insert_eq basis_zero Set.image_singleton basis_one
mem_lattice 📖	mathematical	—	Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Complex.instAdd Complex.instMul Complex.instIntCast ω₁ ω₂	—	zsmul_eq_mul
meromorphic_derivWeierstrassP 📖	mathematical	—	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace derivWeierstrassP	—	deriv_weierstrassP Meromorphic.deriv Complex.instCompleteSpace meromorphic_weierstrassP
meromorphic_weierstrassP 📖	mathematical	—	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace weierstrassP	—	weierstrassPExcept_add AnalyticAt.meromorphicAt analyticOnNhd_weierstrassPExcept MeromorphicAt.fun_add MeromorphicAt.fun_sub MeromorphicAt.fun_div MeromorphicAt.const MeromorphicAt.fun_pow MeromorphicAt.id analyticOnNhd_weierstrassP
mul_ω₁_add_mul_ω₂_mem_lattice 📖	mathematical	—	Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Complex.instAdd Complex.instMul Complex.instRatCast ω₁ ω₂	—	mem_lattice LinearIndependent.pair_iff indep Complex.ofReal_sub Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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.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.mul_one Mathlib.Tactic.Ring.zero_mul 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 Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Rat.cast_intCast RCLike.charZero_rclike CanLift.prf Rat.canLift AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Submodule.addSubmonoidClass Submodule.smul_mem ω₁_mem_lattice ω₂_mem_lattice
not_continuousAt_weierstrassP 📖	mathematical	Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	ContinuousAt weierstrassP	—	weierstrassPExcept_add Iff.not NormedField.continuousAt_zpow zpow_neg one_div add_sub_cancel_left sub_add_cancel ContinuousAt.comp_of_eq ContinuousAt.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousAt.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup DifferentiableAt.continuousAt IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology DifferentiableOn.differentiableAt differentiableOn_weierstrassPExcept compl_lattice_diff_singleton_mem_nhds Continuous.continuousAt continuous_const continuous_add_left add_zero
order_weierstrassP 📖	mathematical	Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	meromorphicOrderAt DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace weierstrassP WithTop WithTop.LinearOrderedAddCommGroup.instNeg Int.instAddCommGroup instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat meromorphicOrderAt_eq_int_iff meromorphic_weierstrassP analyticOnNhd_weierstrassPExcept sub_zero zero_pow Nat.instCharZero div_zero analyticAt_const AnalyticAt.div_const AnalyticAt.fun_pow AnalyticAt.fun_sub analyticAt_id AnalyticAt.fun_add AnalyticAt.fun_mul analyticAt_weierstrassPExcept sub_self MulZeroClass.zero_mul zero_add zero_div NeZero.charZero_one Complex.instCharZero Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass zpow_neg zpow_ofNat ite_eq_one_sub_sq_mul_weierstrassP inv_mul_cancel_left₀
periodic_derivWeierstrassP 📖	mathematical	—	Function.Periodic Complex Complex.instAdd derivWeierstrassP Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	—	derivWeierstrassP_add_coe
periodic_weierstrassP 📖	mathematical	—	Function.Periodic Complex Complex.instAdd weierstrassP Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	—	weierstrassP_add_coe
sumInvPow_zero 📖	mathematical	—	sumInvPow Complex Complex.instZero G	—	sub_zero
summable_weierstrassPExceptSummand 📖	mathematical	Real Real.instLT Norm.norm Complex Complex.instNorm Complex.instSub Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	Summable Complex.instMul weierstrassPExceptSummand Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring SummationFilter.unconditional	—	Metric.isOpen_iff Continuous.isOpen_preimage continuous_mul_right IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsClosed.isOpen_compl IsClosed.upperClosure instOrderTopologyReal isClosedMap_dist Complex.instProperSpace isClosed_of_subset_lattice Set.diff_subset Set.image_congr norm_sub_rev one_mul Nat.instAtLeastTwoHAddOfNat IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instIsOrderedRing Real.instNontrivial dist_add_self_left norm_div abs_eq_self LT.lt.le Real.norm_ofNat MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instZeroLEOneClass RCLike.charZero_rclike mul_comm Equiv.summable_iff Summable.sum IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Denumerable.ofNat_encode Denumerable.encode_ofNat Nat.cast_add neg_add_rev zpow_neg ite_mul MulZeroClass.zero_mul CharP.cast_eq_zero CharP.ofCharZero Complex.instCharZero zero_add Int.instCharZero neg_zero add_zero pow_zero mul_one sub_sq_comm one_div HasSum.summable hasSum_weierstrassPExcept zpow_natCast FormalMultilinearSeries.ofScalars.congr_simp FormalMultilinearSeries.apply_eq_prod_smul_coeff Finset.prod_inv_distrib Finset.prod_const Fintype.card_fin FormalMultilinearSeries.coeff_ofScalars HasFPowerSeriesOnBall.hasSum Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zero edist_zero_right nnnorm_inv abs_inv Summable.mul_right ZLattice.summable_norm_sub_zpow Complex.instFiniteDimensionalReal instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice finrank_lattice IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono Summable.of_norm_bounded Complex.instCompleteSpace Summable.mul_of_nonneg le_of_lt mul_pos Right.add_pos_of_nonneg_of_pos Nat.cast_nonneg' Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo zpow_pos IsStrictOrderedRing.toZeroLEOneClass lt_trans Nat.cast_one mul_nonneg IsOrderedRing.toPosMulMono zpow_nonneg norm_nonneg norm_zero inv_pos_of_pos pow_pos inv_nonneg_of_nonneg sub_self LE.le.not_gt eq_or_ne sub_zero zero_pow MulZeroClass.mul_zero Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_natCast Complex.norm_mul norm_zpow norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors Mathlib.Meta.NormNum.isNat_eq_false Nat.instCharZero Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos 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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.Ring.neg_congr 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.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.add_neg 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.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf zpow_sub₀ div_pow inv_div 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.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.zpow_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt lt_of_le_of_ne' one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono mul_le_mul RCLike.norm_natCast le_refl inv_anti₀ pow_le_pow_left₀ le_div_iff₀ Eq.trans_le pow_nonneg IsOrderedRing.toZeroLEOneClass Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg zpow_ofNat
summable_weierstrassPSummand 📖	mathematical	Real Real.instLT Norm.norm Complex Complex.instNorm Complex.instSub Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	Summable Complex.instMul weierstrassPSummand Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat weierstrassPExceptSummand_of_notMem ω₁_div_two_notMem_lattice summable_weierstrassPExceptSummand
weierstrassPExceptSeries_hasSum 📖	mathematical	Real Real.instLT Norm.norm Complex Complex.instNorm Complex.instSub Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	HasSum Complex.instMul FormalMultilinearSeries.coeff DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace weierstrassPExceptSeries Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring weierstrassPExcept SummationFilter.unconditional	—	Summable.hasSum_iff Complex.instT2Space SummationFilter.instNeBotUnconditional coeff_weierstrassPExceptSeries IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Summable.prod SeminormedAddCommGroup.to_isUniformAddGroup Complex.instCompleteSpace summable_weierstrassPExceptSummand weierstrassPExcept_eq_tsum
weierstrassPExceptSeries_of_notMem 📖	mathematical	Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	weierstrassPExceptSeries weierstrassPSeries	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul SMulCommClass.continuousConstSMul Algebra.to_smulCommClass weierstrassPExcept_of_notMem sub_zero
weierstrassPExceptSummand_of_notMem 📖	mathematical	Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	weierstrassPExceptSummand weierstrassPSummand	—	—
weierstrassPExcept_add 📖	mathematical	—	Complex Complex.instAdd weierstrassPExcept Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Complex.instSub DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring weierstrassP	—	one_div tsum_ite_eq SummationFilter.instLeAtTopUnconditional weierstrassPExcept.eq_1 Summable.tsum_add Complex.instT2Space IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SummationFilter.instNeBotUnconditional hasSum_weierstrassPExcept summable_of_finite_support SummationFilter.instHasSupportOfLeAtTop Set.Finite.subset Set.finite_singleton zero_add add_zero
weierstrassPExcept_def 📖	mathematical	—	weierstrassPExcept Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Complex.instAdd weierstrassP Complex.instSub DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring	—	weierstrassPExcept_add Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg
weierstrassPExcept_eq_tsum 📖	mathematical	Real Real.instLT Norm.norm Complex Complex.instNorm Complex.instSub Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	weierstrassPExcept tsum Complex.instMul FormalMultilinearSeries.coeff DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace weierstrassPExceptSeries Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring SummationFilter.unconditional	—	tsum_zero one_div Nat.instAtLeastTwoHAddOfNat Nat.cast_add neg_add_rev zpow_neg mul_comm IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing add_sub_cancel FormalMultilinearSeries.ofScalars.congr_simp FormalMultilinearSeries.apply_eq_prod_smul_coeff Finset.prod_const Fintype.card_fin FormalMultilinearSeries.coeff_ofScalars HasSum.tsum_eq Complex.instT2Space SummationFilter.instNeBotUnconditional HasFPowerSeriesOnBall.hasSum Complex.one_div_sub_sq_sub_one_div_sq_hasFPowerSeriesOnBall_zero LE.le.trans_lt norm_nonneg Metric.eball_coe dist_zero_right ite_mul MulZeroClass.zero_mul coeff_weierstrassPExceptSeries IsTopologicalRing.toIsTopologicalSemiring Summable.tsum_comm SeminormedAddCommGroup.to_isUniformAddGroup Complex.instCompleteSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace summable_weierstrassPExceptSummand
weierstrassPExcept_neg 📖	mathematical	—	weierstrassPExcept Complex Complex.instNeg	—	Equiv.tsum_eq sub_neg_eq_add one_div Even.neg_pow Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_pf_left 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.add_pf_add_gt Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf
weierstrassPExcept_of_notMem 📖	mathematical	Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	weierstrassPExcept weierstrassP	—	one_div
weierstrassPExcept_zero 📖	mathematical	—	weierstrassPExcept Complex Complex.instZero	—	zero_sub Even.neg_pow Nat.instAtLeastTwoHAddOfNat one_div sub_self tsum_zero
weierstrassPSeries_hasSum 📖	mathematical	Real Real.instLT Norm.norm Complex Complex.instNorm Complex.instSub Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	HasSum Complex.instMul FormalMultilinearSeries.coeff DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace weierstrassPSeries Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring weierstrassP SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul weierstrassPExceptSeries_of_notMem ω₁_div_two_notMem_lattice weierstrassPExcept_of_notMem weierstrassPExceptSeries_hasSum
weierstrassP_add_coe 📖	mathematical	—	weierstrassP Complex Complex.instAdd Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	—	add_zero neg_add_cancel_right lattice.eq_1 Submodule.span_le ω₁_mem_lattice ω₁_div_two_notMem_lattice ω₂_mem_lattice ω₂_div_two_notMem_lattice
weierstrassP_bound 📖	mathematical	Real Real.instLT Real.instZero Norm.norm Complex Complex.instNorm Real.instLE Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Complex.instSub DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Real.instPow Real.instNeg	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.atom_pf 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_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.instAtLeastTwo 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.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le lt_of_not_ge Mathlib.Tactic.Linarith.mul_neg Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike div_sub_div isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero one_mul mul_one Complex.norm_div Complex.norm_mul norm_pow NormedDivisionRing.to_normOneClass div_le_div₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono norm_nonneg le_refl mul_pos pow_pos IsStrictOrderedRing.toZeroLEOneClass div_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono pow_le_pow_left₀ IsOrderedRing.toPosMulMono le_of_lt norm_sub_rev LE.le.trans le_of_not_gt Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.isNat_mul norm_sub_norm_le sq_sub_sq add_sub_cancel sub_add_eq_add_sub two_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Meta.NormNum.isNNRat_pow Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Meta.NormNum.one_natPow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Mathlib.Meta.NormNum.isNat_eq_false ne_of_gt one_ne_zero NeZero.one GroupWithZero.toNontrivial div_le_div_of_nonneg_right mul_le_mul mul_le_mul_of_nonneg_left norm_sub_le Complex.norm_ofNat CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true Mathlib.Meta.NormNum.isNNRat_ratCast Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_mkRat Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsNat.raw_refl Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.natPow_one Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_intOfNat Rat.instCharZero CancelDenoms.mul_subst CancelDenoms.add_subst Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.Ring.cast_nnrat Real.rpow_intCast
weierstrassP_coe 📖	mathematical	—	weierstrassP Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice Complex.instZero	—	zero_add weierstrassP_add_coe weierstrassP_zero
weierstrassP_neg 📖	mathematical	—	weierstrassP Complex Complex.instNeg	—	Equiv.tsum_eq sub_neg_eq_add one_div Even.neg_pow Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_pf_left 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.add_pf_add_gt Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf
weierstrassP_sub_coe 📖	mathematical	—	weierstrassP Complex Complex.instSub Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice	—	weierstrassP_add_coe sub_add_cancel
weierstrassP_zero 📖	mathematical	—	weierstrassP Complex Complex.instZero	—	zero_sub Even.neg_pow Nat.instAtLeastTwoHAddOfNat one_div sub_self tsum_zero
ω₁_div_two_notMem_lattice 📖	mathematical	—	Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice DivInvMonoid.toDiv Complex.instDivInvMonoid ω₁ instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat one_div Rat.cast_inv Complex.instCharZero Rat.cast_ofNat inv_mul_eq_div Rat.cast_zero MulZeroClass.zero_mul add_zero Iff.not mul_ω₁_add_mul_ω₂_mem_lattice Mathlib.Meta.NormNum.isNat_eq_false Nat.instCharZero Tactic.NormNum.isNat_ratDen Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNNRat_inv_pos Rat.instCharZero Mathlib.Meta.NormNum.isNat_eq_true
ω₁_mem_lattice 📖	mathematical	—	Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice ω₁	—	Submodule.subset_span
ω₂_div_two_notMem_lattice 📖	mathematical	—	Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice DivInvMonoid.toDiv Complex.instDivInvMonoid ω₂ instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Rat.cast_zero MulZeroClass.zero_mul one_div Rat.cast_inv Complex.instCharZero Rat.cast_ofNat inv_mul_eq_div zero_add Iff.not mul_ω₁_add_mul_ω₂_mem_lattice Mathlib.Meta.NormNum.isNat_eq_true Tactic.NormNum.isNat_ratDen Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_eq_false Nat.instCharZero Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos Rat.instCharZero
ω₂_mem_lattice 📖	mathematical	—	Complex Submodule Int.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup AddCommGroup.toIntModule Complex.addCommGroup SetLike.instMembership Submodule.setLike lattice ω₂	—	Submodule.subset_span

(root)

Definitions

Name	Category	Theorems
PeriodPair 📖	CompData	—

---

← Back to Index