Transform

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

Statistics

Metric	Count
Definitions	0
Theorems E2_slash_action, G2_S_transform, G2_T_transform, G2_slash_action	4
Total	4

EisensteinSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
E2_slash_action 📖	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 E2 Pi.instSub Complex.instSub Function.hasSMul Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat riemannZeta D2	—	Nat.instAtLeastTwoHAddOfNat one_div mul_inv_rev ModularForm.SL_smul_slash IsScalarTower.right G2_slash_action mul_sub
G2_S_transform 📖	mathematical	—	G2 Complex Complex.instSub Complex.instMul Complex.instInv Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring UpperHalfPlane.coe Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction UpperHalfPlane.SLAction Ring.toIntAlgebra Real Real.instRing ModularGroup.S DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I	—	Nat.instAtLeastTwoHAddOfNat
G2_T_transform 📖	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 ModularGroup.T G2	—	ModularForm.SL_slash_def UpperHalfPlane.modular_T_smul Nat.instAtLeastTwoHAddOfNat G2_eq_tsum_cexp Matrix.cons_val' Matrix.cons_val_fin_one Int.cast_zero MulZeroClass.zero_mul Int.cast_one zero_add zpow_neg one_zpow inv_one mul_one Function.Periodic.nat_mul Complex.exp_periodic Nat.cast_one one_mul IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Complex.instCharZero isReduced_of_noZeroDivisors Nat.instCharZero
G2_slash_action 📖	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 G2 Pi.instSub Complex.instSub D2	—	SpecialLinearGroup.SL2Z_generators Subgroup.closure_induction UpperHalfPlane.im_inv_neg_coe_pos Nat.instAtLeastTwoHAddOfNat SlashInvariantForm.slash_S_apply mul_comm G2_S_transform UpperHalfPlane.modular_S_smul D2_S Mathlib.Tactic.Ring.inv_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.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_inv_neg Complex.instCharZero Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg mul_one add_zero 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.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.div_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add zpow_neg inv_pow IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero instIsDomain D2_T sub_zero G2_T_transform SlashAction.slash_one D2_one D2_mul SlashAction.slash_mul sub_eq_add_neg SlashAction.add_slash SlashAction.neg_slash mul_inv_cancel D2_inv ModularForm.SL_slash sub_neg_eq_add add_sub_cancel_right

---

← Back to Index