diff --git a/set.mm b/set.mm index fd7138ce9..1d975f5c5 100644 --- a/set.mm +++ b/set.mm @@ -630930,7 +630930,7 @@ standardize vectors to a length (norm) of one, but such definitions require anpnaneq0d.2 $e |- ( ph -> N e. NN0 ) $. anpnaneq0d.3 $e |- ( ph -> -. 2 || N ) $. $( The sum of a real number to the power of N and the negative of the - number to the power of N equals zero if N is a nonnegative even integer. + number to the power of N equals zero if N is a nonnegative odd integer. (Contributed by Igor Ieskov, 21-Jan-2024.) $) anpnaneq0d $p |- ( ph -> ( ( A ^ N ) + ( -u A ^ N ) ) = 0 ) $= ( cexp co cneg caddc cc0 wceq recnd mulm1d oveq1d wcel wi a1i mpd eqtr4d