IndisputableMonolith.Mathematics.ImaginaryUnit

declarations in this module (15)

• def eightTickPhase L51
• theorem tick2_is_i L55
• theorem tick4_is_neg1 L64
• theorem i_is_rotation L75
• theorem two_rotations L84
• theorem i_squared_from_8tick L93
• theorem i_power_is_rotation L98
• def whyComplex L116
• theorem schrodinger_i_from_8tick L134
• theorem euler_from_8tick L156
• theorem euler_identity L166
• def implications L178
• def rootOfUnity L191
• theorem roots_form_group L195
• structure ImaginaryUnitFalsifier L225