Skip to content

Commit

Permalink
Specify N must be odd in anpnaneq0d.
Browse files Browse the repository at this point in the history
  • Loading branch information
igorocky committed Jan 21, 2024
1 parent 45d7d50 commit 9f2906a
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion set.mm
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 9f2906a

Please sign in to comment.