Commit 2025-05-14 18:50 73a7031f
View on Github →feature(Analysis/SpecialFunctions/Complex/CircleAddChar): ZMod.toCircle_eq_circleExp (#24463)
Show that ZMod.toCircle k equals Circle.exp (2 * π * (k.val / N)).
feature(Analysis/SpecialFunctions/Complex/CircleAddChar): ZMod.toCircle_eq_circleExp (#24463)
Show that ZMod.toCircle k equals Circle.exp (2 * π * (k.val / N)).