You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Commit 86af577
Browse filesBrowse the repository at this point in the historyBrowse files
A congruence is solved to a residue class, two classes meet by the Chinese remainder theorem, the modular inverse is a class representative, lcm is a function, and a quantified statement over the whole numbers is decided by its residues (#1424)
Item 3 of the #1409 docket, chapter 6's number theory on top of the congruence node, and
#180's "proper modular arithmetic".
A residue class is the set { x in ZZ : x = r (mod n) }, r in [0, n), and everything here is
arithmetic on those. Solve reads a x + b = c (mod n) through the gcd: solutions exactly when
gcd(a, n) divides c - b, one class modulo n / gcd -- 3 x = 11 (mod 7) is { x in ZZ : x = 6
(mod 7) }, 2 x = 4 (mod 6) is x = 2 (mod 3), 2 x = 3 (mod 6) has none -- and a congruence of
higher degree by the residues that satisfy it. Two classes intersect by the Chinese remainder
theorem, with the coprime case as the case where the consistency condition a = b (mod gcd) is
empty: x = 3 (mod 4) and x = 5 (mod 6) is x = 11 (mod 12), x = 3 (mod 4) and x = 2 (mod 6) is
nothing, x = 2 (mod 6) and x = 5 (mod 9) is x = 14 (mod 18). A class cut down by a bounded
interval is the finite set of its members, so the book's coins -- x = 1 (2), 1 (3), 2 (5),
between 250 and 300 -- come out as { 277 }; an intersection A /\ [a; +oo) /\ (-oo; b] is
regrouped so that the two intervals meet first. MathS.NumberTheory.ModularInverse(a, n) is the
one representative in [1, n - 1], or null where a and n share a factor: a class, never 1/a.
lcm(a, b, ...) is a node by gcd's conventions -- non-negative, 0 where either is 0,
lcm(a/b, c/d) = lcm(a, c) / gcd(b, d) -- where it was refused by name.
Two more routes for a quantifier over ZZ, ZZ* or ZZ+. A body that is a divisibility by a whole
number or a congruence modulo one, of polynomials with whole coefficients, joined by the
connectives, repeats with the modulus, so its residues decide it: forall n in ZZ : 6 divides
n^3 + 5 n is six cases (Ex 6.5.14), forall p in ZZ : (not 2 divides p and not 3 divides p)
implies p^2 = 1 (mod 24) twenty-four, and a nested quantifier over whole numbers is decided at
each residue of the outer one. And a polynomial equation with no solution modulo some small m
has none in the whole numbers -- exists x, y in ZZ : 3 x^2 - 5 y^2 = 1 is False because
x^2 = 2 (mod 5) has no solution (Ex 6.5.27), x^2 - y^2 = 14 by parity -- while a solution modulo
every m tried proves nothing and is not read as one.
Every spelling but lcm was a parse error in 2.5.0; recorded in BREAKING-CHANGES.md.
Part of #1409. Part of #180.
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Copy file name to clipboardExpand all lines: Sources/AngouriMath/Core/Antlr/AngouriMath.g
+1-1Lines changed: 1 addition & 1 deletion
Original file line number
Diff line number
Diff line change
@@ -558,6 +558,7 @@ atom returns[Entity value]
558
558
| 'argmax(' args = function_arguments ')' { Assert("argmax", 2, $args.list.Count); $value = $args.list[1] is Entity.Set.Inf { Element: Variable } argmaxRange ? MathS.Argmax($args.list[0], argmaxRange.Element, argmaxRange.SupSet) : throw new InvalidArgumentParseException("argmax expects its second argument to say which variable ranges over which set, as in argmax(f(t), t in S)"); }
559
559
| 'argmin(' args = function_arguments ')' { Assert("argmin", 2, $args.list.Count); $value = $args.list[1] is Entity.Set.Inf { Element: Variable } argminRange ? MathS.Argmin($args.list[0], argminRange.Element, argminRange.SupSet) : throw new InvalidArgumentParseException("argmin expects its second argument to say which variable ranges over which set, as in argmin(f(t), t in S)"); }
0 commit comments