Assumptions:
TeX:
j\!\left(\tau + 1\right) = j(\tau)
\tau \in \mathbb{H}Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| ModularJ | Modular j-invariant | |
| HH | Upper complex half-plane |
Source code for this entry:
Entry(ID("a997f2"),
Formula(Equal(ModularJ(Add(tau, 1)), ModularJ(tau))),
Variables(tau),
Assumptions(Element(tau, HH)))