Defs

📁 Source: Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Defs.lean

Statistics

Metric	Count
Definitions D2, E2, e2Summand	3
Theorems D2_S, D2_T, D2_inv, D2_mul, D2_one, e2Summand_even, e2Summand_summable, e2Summand_zero_eq_two_riemannZeta_two	8
Total	11

EisensteinSeries

Definitions

Name	Category	Theorems
D2 📖	CompOp	7 math math: E2_slash_action, G2_slash_action, D2_S, D2_inv, D2_one, D2_T, D2_mul
E2 📖	CompOp	2 math math: E2_slash_action, ModularForm.logDeriv_eta_eq_E2
e2Summand 📖	CompOp	8 math math: hasSum_e2Summand_symmetricIcc, e2Summand_even, G2_eq_tsum_symmetricIco, tendsto_e2Summand_atTop_nhds_zero, hasSum_e2Summand_symmetricIco, e2Summand_zero_eq_two_riemannZeta_two, summable_e2Summand_symmetricIcc, summable_e2Summand_symmetricIco

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
D2_S 📖	mathematical	—	D2 ModularGroup.S Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I UpperHalfPlane.coe	—	Nat.instAtLeastTwoHAddOfNat Matrix.cons_val' Matrix.cons_val_fin_one Int.cast_one mul_one one_mul Int.cast_zero add_zero
D2_T 📖	mathematical	—	D2 ModularGroup.T Pi.instZero UpperHalfPlane Complex Complex.instZero	—	Matrix.cons_val' Matrix.cons_val_fin_one Int.cast_zero MulZeroClass.mul_zero zero_div
D2_inv 📖	mathematical	—	SlashAction.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.monoid Pi.addMonoid UpperHalfPlane Complex ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ModularForm.SLAction Matrix.SpecialLinearGroup.hasInv D2 Pi.instNeg Complex.instNeg	—	mul_inv_cancel D2_one D2_mul
D2_mul 📖	mathematical	—	D2 Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.hasMul Pi.instAdd UpperHalfPlane Complex Complex.instAdd SlashAction.map Matrix.SpecialLinearGroup.monoid Pi.addMonoid ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ModularForm.SLAction	—	mul_assoc map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass ModularForm.SL_slash_def zpow_neg Distrib.leftDistribClass IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain Complex.instCharZero Matrix.SpecialLinearGroup.det_coe Int.cast_one mul_one UpperHalfPlane.im_pos UpperHalfPlane.coe_specialLinearGroup_apply eq_intCast RingHom.instRingHomClass UpperHalfPlane.specialLinearGroup_apply Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg UpperHalfPlane.denom_ne_zero Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.zpow_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial pow_two UpperHalfPlane.denom_cocycle UpperHalfPlane.im_ne_zero Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_congr 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.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_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
D2_one 📖	mathematical	—	D2 Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.hasOne Pi.instZero UpperHalfPlane Complex Complex.instZero	—	Matrix.one_apply_ne Fin.instNeZeroHAddNatOfNat_mathlib_1 Int.cast_zero MulZeroClass.mul_zero map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass zero_div
e2Summand_even 📖	mathematical	—	Function.Even Complex e2Summand	—	tsum_comp_neg tsum_congr Int.cast_neg neg_mul Matrix.cons_val_fin_one zpow_neg zpow_natCast Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul 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.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.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_one
e2Summand_summable 📖	mathematical	—	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup eisSummand Matrix.vecCons Matrix.vecEmpty SummationFilter.unconditional	—	Summable.congr linear_right_summable Matrix.cons_val_fin_one zpow_neg
e2Summand_zero_eq_two_riemannZeta_two 📖	mathematical	—	e2Summand Complex Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat riemannZeta	—	Nat.instAtLeastTwoHAddOfNat Int.cast_zero MulZeroClass.zero_mul Matrix.cons_val_fin_one zero_add zpow_neg two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even

---

← Back to Index