Assumptions:
TeX:
j\!\left(\frac{a \tau + b}{c \tau + d}\right) = j\!\left(\tau\right) \tau \in \mathbb{H} \,\mathbin{\operatorname{and}}\, \begin{pmatrix} a & b \\ c & d \end{pmatrix} \in \operatorname{SL}_2(\mathbb{Z})
Definitions:
Fungrim symbol | Notation | Short description |
---|---|---|
ModularJ | Modular j-invariant | |
HH | Upper complex half-plane | |
Matrix2x2 | Two by two matrix | |
SL2Z | Modular group |
Source code for this entry:
Entry(ID("d5f569"), Formula(Equal(ModularJ(Div(Add(Mul(a, tau), b), Add(Mul(c, tau), d))), ModularJ(tau))), Variables(a, b, c, d, tau), Assumptions(And(Element(tau, HH), Element(Matrix2x2(a, b, c, d), SL2Z))))