Repository navigation
Update to latest HOL Light master - #20
Merged
Merged
Conversation
Calling define_record_type twice with the same specification previously failed with "new_basic_type_definition: Constant(s) already in use", because it unconditionally re-ran define_type_raw and new_specification. Add a dedicated the_record_types cache keyed on the parsed (tyname, fields): a repeat with identical fields returns the cached theorems (warning "Benign redefinition of record type"), while a repeat with the same type name but different fields fails with a clear message rather than a low-level kernel error. Move the record-type tests out of UnitTests/basic_tests.ml into a new UnitTests/records.ml (wired into the Makefile and CI), and add tests for the benign-redefinition and clashing-redefinition behaviour. Document define_record_type and define_auto_record_type under Help/. Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…rh13#199) This is fully backward compatible: existing `hol-mcp.toml` files and every current `hol_restart`/`hol_status` behavior are unchanged. The new behavior is entirely opt-in via new arguments, so no existing HOL Light user is affected. Reworks the MCP server's `hol_restart` from a bare kill/restart into a config-aware restart, so an agent editing an underlying source file can refresh its environment without dropping the session. `hol_restart` now reloads `hol-mcp.toml`, accepts a one-shot `checkpoint=` override, and (with `rebuild_hol_and_checkpoint=true`) can rebuild HOL Light and the selected checkpoint in place. `hol_status` gains active-vs-configured checkpoint, startup mode, and stale-checkpoint reporting. See README/hol-mcp.toml for the config format and semantics. Points for review: - The rebuild shells out to `make clean`/`make` and replaces checkpoint files. It is gated behind an explicit, non-default flag, builds into a temp dir so a failed build never touches the live checkpoint, and on any later failure quarantines HOL (rejecting proof work with a recovery message) rather than falling back to a stale checkpoint. - Only the `base` checkpoint may be rebuilt without a recipe; any other checkpoint without a `[checkpoint_recipes.<name>]` entry fails, so a custom checkpoint is never silently rebuilt as bare HOL. Defining a recipe is the only reason to touch an existing config. New test_restart.py covers reload, override, recipe validation, failure handling/quarantine, and progress reporting; test_server.py/smoke_test.py and CI are updated. Verified from a clean build (OCaml 5.4.0): 63 unit tests and 37/37 smoke checks pass.
…3#200) While looking into OCaml 5.5 support: this branch of chooser.sh required OCaml 5.4 exactly and returned UNKNOWN otherwise, so the build failed. Select the grammar on the camlp5 version alone, and rename the file accordingly. Tested every OCaml 5.x release that these camlp5 versions support, plus 4.14: camlp5 8.05.02 OCaml 4.14.4, 5.0.0, 5.1.1, 5.2.1, 5.3.0, 5.4.1, 5.5.0 camlp5 8.04.00 OCaml 4.14.4, 5.0.0, 5.1.1, 5.2.1, 5.3.0, 5.4.1 In all thirteen combinations chooser.sh selects pa_j_8.04.00.ml, "HOLLIGHT_USE_MODULE=1 make" completes, and all four unit test binaries pass: UnitTests/basic_tests and UnitTests/printer_tests, native and bytecode, with the printer tests reporting 107/107. Before this change only OCaml 5.4 built. camlp5 8.04.00 does not support OCaml 5.5, so that combination cannot occur. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
planar embedding theorem, the latter together with much other material on planar graphs including equivalent combinatorial characterizations. The hilbert_waring.ml formalization, produced by Claude Opus 4.8, proves Hilbert's solution of Waring's problem: for each positive exponent e there is a bound k(e) such that every natural number is a sum of k(e) e-th powers. The proof follows Linnik's elementary method as presented in Khinchin's "Three Pearls of Number Theory", chapter 3. It develops the difference-polynomial and fiber-counting induction behind Khinchin's fundamental lemma, obtains positive Schnirelmann density for a bounded sumset of e-th powers, and applies the existing Schnirelmann density-to-basis theorem. The planar_graph.ml formalization, produced by GPT-5.6-sol (xhigh), develops a general theory of finite simple planar graphs over an arbitrary vertex type, with edges represented as two-element sets and planarity defined using non-crossing arcs in the plane. It proves Fary's straight-line embedding theorem, equivalent recursive-triangulation and Euler-rotation characterizations of planarity, Euler's formula and the planar edge bound, Kuratowski's theorem in terms of K5 and K3,3 subdivisions, and Wagner's theorem in terms of the corresponding forbidden minors. It also supplies reusable results about graph minors, degrees and degeneracy, relabelling, components, closure operations and amalgamation. The proof of Fary's theorem follows the maximal-triangulation and recursive-disk approach in Jeff Erickson's "Planar Graphs" notes, itself following de Fraysseix, Pach and Pollack. The Kuratowski development uses rotation systems, Thomassen's contractible-edge theorem and separator induction.
This patch factors out TacticTrace that makes it easier to update the OCaml version of HOL Light. It now lives at https://github.com/hol-light/TacticTrace Remove the directory and drop the corresponding TacticTrace/make-test target from holtest.mk. The new repository tests the same thing in its own GitHub Actions workflows, and additionally checks the collected traces against the expected output in its examples/*.answer directories. Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Make a type-annotated binder shadow a like-named constant * Let a binder also shadow an interface or overloaded name The fix in "Make a type-annotated binder shadow a like-named constant" made a varstruct name that is also a constant be pre-bound as a variable before the varstruct is typed, so that type annotations and tuples are handled. But it recognized such names with "get_const_type", whereas the Varp branch of "typify" decides that a name denotes a constant with "not(is_hidden s) && can get_generic_type s". The two differ on interface and overloaded names such as "gcd", "sum" or "norm", which are not themselves constants: for those, "\gcd. t" silently became a degenerate generalized abstraction rather than a plain abstraction, contrary to "ignore_constant_varstruct", and "\(gcd:num). t" failed to typecheck. So use the same test as "typify" in varstruct_consts. Also annotate the venv and uenv operands of "typify" with their types and briefly comment the shadowing code, and restore the file-final newline of preterm.ml. The constant-shadowing tests move from UnitTests/basic_tests.ml to a new UnitTests/parser_tests.ml, for checks on the parsing and typechecking of quotations, with the interface-name cases added; it is built by "make" and run in CI alongside the basic and printer suites. Co-authored-by: Claude Opus 5 <noreply@anthropic.com> * Add missing backslash --------- Co-authored-by: Juneyoung Lee <lebjuney@amazon.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com> Co-authored-by: Juneyoung Lee <136006969+aqjune-aws@users.noreply.github.com>
Changed "make switch" and "make switch-5" to pin camlp5 before installing ledit rather than after. Since ledit depends on camlp5, installing it first pulled in the latest camlp5 (8.05.02), so the pin then downgraded camlp5 and made OPAM rebuild ledit. With OPAM 2.6 that rebuild fails with "No rule to make target `all'": when a package with a "remove:" field, as ledit has, must be removed before it is rebuilt, as here, OPAM 2.6 moves the downloaded sources into a directory for the removal and then runs the build in an empty directory. OPAM 2.5 and earlier are not affected, but Homebrew now provides OPAM 2.6, so this showed up in the macOS CI of s2n-bignum. Now ledit is just built once, against the pinned camlp5. The pin and the install are also now joined by "&&", so that a failed pin is reported rather than leaving an unpinned camlp5, and "eval $(opam env)" is now "eval $$(opam env)", since make was expanding "$(opam env)" itself (to nothing).
…13#207) Fixes to holtest.mk's test list/rules, plus a cleanup of holtest_parallel: 1. Examples/apery: the TESTS list referenced 'Library/apery', but the file lives at Examples/apery.ml (added in 6868f3c). The generic rule's 'loadt "Library/apery.ml"' therefore found nothing, raised a stray 'Exception: Not_found.', and -- because that is not reported as a load failure -- still touched the .ready marker, so the test silently passed without proving anything. Point it at Examples/apery. 2. Mizarlight/make: make.ml loads Mizarlight/pa_f.cmo (a camlp5 syntax extension providing infixes like THEN'), but nothing built it when the test was driven via holtest.mk's generic rule. The load then had no effect and miz2a.ml failed with 'Unbound value THEN''. Add a dedicated rule that runs 'make -C Mizarlight pa_f.cmo' before loading make.ml. 3. holtest_parallel: drop the leading binary-selection/build block. The 'ckpt' (checkpoint) path no longer works, and the from-source branch's 'make clean' would delete the HOLLIGHT_USE_MODULE=1 module binaries before the run. The script now assumes HOL Light is already built and relies on holtest.mk's default HOLLIGHT=./hol.sh. The Mizarlight build it used to do is now handled by holtest.mk (see 2).
The MCP server now lives at https://github.com/hol-light-family/hol-light-mcp with its history preserved. Replace mcp/ with a README pointing there, and drop the MCP CI workflow and dependabot entry.
mainly Opus 5.5: * Autoformalization/carleson_hunt.ml is the Carleson-Hunt extension to all L^p for p > 1 of the existing Carleson theorem, which is the special case p = 2: the Fourier series for an L^2 periodic function converges a.e. * Autoformalization/puiseux.ml is Puiseux's theorem, that for an algebraically closed field k of characteristic zero, the field of Puiseux series over k is algebraically closed. * Autoformalization/godel_*.ml collectively prove the independence from the axioms of ZF set theory of the continuum hypothesis, the generalized continuum hypothesis and the axiom of choice. * 4CT/* proves the 4-colour theorem, in the classical setting of planar maps and also for planar graphs etc. It is a direct port of Gonthier's original Coq proof, except for the high-level topological link which is done slightly differently. The 4CT proof uses Alexey Solovyev's machinery for compiling equational theorems into efficient conversions for evaluation by inference, which is now included in the distribution in the eval_compile subdirectory. This update also fixes a number of errors in the Help entries that were pointed out by Chris Walton.
* Move the OCaml 5 build target from OCaml 5.4 to OCaml 5.5
'make switch-5' now creates a switch with OCaml 5.5.2, the newest OCaml release
in OPAM, and the CI job that exercises it follows suit. No new version-specific
sources are needed: the existing pa_j/pa_j_8.04.00.ml already covers camlp5
8.05, and the compiler-libs interfaces that update_database/update_database_5.4.ml
relies on (Env.fold_values/fold_modules, Longident and Toploop) are unchanged in
OCaml 5.5, so the update_database selector just has to accept 5.5 as well. OCaml
5.4 remains supported.
The 'switch' and 'switch-5' targets no longer carry their own list of packages
to install with camlp5 pinned to a hardwired version; they now ask OPAM for the
dependencies recorded in the opam file ('opam install . --deps-only'), so that
the supported combinations of OCaml and camlp5 versions are written down in one
place only. This takes three changes to the opam file and one more step in the
switch targets:
- The OCaml >= 4.14 alternatives become a single one accepting any camlp5 from
8.0, and the camlp5 bound for each compiler series is stated as a condition
of its own: at most 8.03.06 on OCaml 4.14 to 5.3, exactly 8.04.00 on 5.4,
and 8.05 to 8.05.03 on 5.5. Those are the newest versions that this tree has
been built and tested with, which is tighter than what camlp5's own metadata
would allow on these compilers, because pa_j/chooser.sh maps a camlp5
version to a pa_j source file and a release it does not know about asks for
a file that does not exist. The bound for 5.4 was also wrong before in
asking for the nonexistent version "8.04" exactly rather than for a version
in the 8.04 series.
Conditions rather than alternatives of their own because OPAM compiles the
whole formula to CNF, where the number of clauses is the product of the
sizes of the alternatives: the eight-alternative form of this file overflows
the solver's stack in the OPAM 2.1 that Ubuntu 22.04 ships, whereas a
condition adds a couple of clauses and leaves room for the next compiler.
- After the '--deps-only' step, the switch targets pin camlp5 to the version
that OPAM just installed ('opam pin add -y -n camlp5 $(opam var
camlp5:version)'). The opam file constrains camlp5 only while the
dependencies are being resolved, and HOL Light itself is not installed in
the switch, so without the pin an 'opam upgrade' is free to move camlp5 out
of the range the opam file asks for: on a fresh OCaml 4.14 switch it
replaces camlp5 8.03.06 with 8.05.03, an untested combination, and a future
camlp5 8.06 would leave pa_j/chooser.sh asking for a pa_j file that does not
exist. Pinning the version that is already installed means nothing is
rebuilt.
- The version becomes "3.1.0+", as in META, rather than "3.1.0". OPAM 2.1
otherwise resolves the dependencies of a checkout against the metadata of
the released hol_light.3.1.0 package of the same version number, which caps
camlp5 below 8.04 and so cannot be satisfied on an OCaml 5 switch at all.
The first and the last of those are OPAM behaviour that is easy to trip over
when adding a compiler or preparing a release, so each is noted in a comment in
the opam file as well. For the same one-place reason as above, the README no
longer lists the compatible OCaml and camlp5 versions itself and refers to the
opam file instead.
Also adds the build products of UnitTests/records.ml to .gitignore, which
listed those of the other three unit tests but not these.
Tested with a clean 'make switch-5', which gives OCaml 5.5.2 with camlp5
8.05.03, zarith 1.14 and ledit 2.08, followed by 'make' in both the default and
the HOLLIGHT_USE_MODULE=1 configurations: all four UnitTests pass in bytecode
and native, update_database.ml loads, and Library/words.ml loads. The 'make
switch' path was checked the same way and still selects OCaml 4.14.0 with camlp5
8.03.06, the version it used to pin by hand; 'make switch-5' does install a
different camlp5 than before, 8.05.03 on OCaml 5.5.2 where it used to install
8.04.00 on OCaml 5.4.
The dependency formula was also checked to resolve, without overflowing the
solver, on an OCaml 5.4 switch (camlp5 8.04.00), on an OCaml 5.5 switch
(8.05.03), and on an empty switch where OPAM has to choose the compiler as
well, both as it stands and with a fourth condition added for a hypothetical
OCaml 5.6. The pin was checked on a fresh OCaml 4.14.0 switch, where 'opam
upgrade' moves camlp5 from 8.03.06 to 8.05.03 without it and is a no-op with
it.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Fix 'make switch' exit status, cap camlp5 on OCaml 4.10 to 4.13
The 'switch' and 'switch-5' targets joined the camlp5 pin to the dependency
install with ';', so the pin ran even when the install had failed and, being
the last command of the recipe, decided the exit status that make sees. If
camlp5 installed but zarith or ledit did not, for want of GMP say, 'make
switch' reported success; and if camlp5 itself failed, OPAM's own error was
followed by a confusing 'Ambiguous argument "camlp5"' from the pin. The two are
joined with '&&' now, so a failed install fails the target and the pin does not
run.
The camlp5 upper bound that the opam file imposes from the OCaml 4.14 series
onwards now starts at the 4.10 series instead, whose alternative asks for
"camlp5" {>= "7.14"} with no upper bound of its own. OPAM does not actually
pick a camlp5 that new there when resolving this file from scratch, because
camlp5 is only a dependency and the solver prefers 8.00.04, which pulls in far
fewer packages than 8.05.03 does. But 8.05.x is installable on those compilers
and is accepted on a switch that already carries it, and pa_j/chooser.sh has
never been exercised with that combination.
Tested on an OCaml 4.13.1 switch carrying camlp5 8.05.03, where 'opam install .
--deps-only' now offers to downgrade camlp5 to 8.03.06 and accepted 8.05.03
before this change. A fresh resolve on that switch selects camlp5 8.00.04 with
or without the bound, and the OCaml 5.4 and 5.5 switches are unaffected, still
resolving to camlp5 8.04.00 and 8.05.03.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
…nite
fields, determinants over commutative rings, much more commutative algebra
and field theory, and the unsolvability of the quintic by radicals. The
majority of this material was automatically developed by Claude Code, with
some human contributions mixed in (probably about 20%).
* Library/galois.ml (new) is Galois theory for field extensions given by
arbitrary homomorphisms: Galois groups, fixed fields and Artin's
theorem, the fundamental theorem for finite Galois extensions, natural
irrationalities, Galois groups of polynomials (transposition,
discriminant and cubic criteria) and of finite fields, Hilbert 90,
Kummer and Artin-Schreier extensions, radical extensions, and in
characteristic zero the equivalence of solvability by radicals with
solvability of the Galois group. Library/cyclotomic.ml (new) embeds
the Galois group of a cyclotomic extension in the units modulo n.
* 100/unsolvability.ml (new) proves that no root of x^5 - 4x + 2 can be
expressed by radicals, number 16 of the 100 theorems.
* Library/fieldtheory.ml is substantially extended with extension
degrees, minimal polynomials, splitting, normal, separable, perfect and
purely inseparable extensions, separable and inseparable degrees,
normal closures, the primitive element theorem, the trace and norm of
finite extensions, and the existence and uniqueness of finite fields of
each prime power order. It now also loads Library/ring_det.ml.
* Library/ring_det.ml (new) has determinants of square arrays over any
commutative ring indexed by any finite set, characteristic polynomials,
the trace, norm and discriminant of algebras with a finite projective
or free basis, and resultants and discriminants of polynomials.
* Library/finite_fields.ml (new) has primitive roots, subfields and
homomorphisms, norm and trace, Hilbert 90, irreducible polynomials and
their counts, and Rabin's irreducibility test, which moves here from
Library/rabin_test.ml (now deleted).
* Library/ringtheory.ml gains radicals and minimal primes, localization
maps, fields of fractions, residue fields, restricted products,
splitting and separable polynomials, roots of unity and many smaller
results, and Library/ring_groups.ml (new) has the additive group and
the unit group of a ring.
* Library/grouptheory.ml gains the second and third isomorphism
theorems, cosets, inverse limits, restricted products and Iwasawa's
criterion. There are smaller additions to Library/symmetric_group.ml,
permutations.ml, matroids.ml, card.ml, iter.ml and wo.ml, and to the
core files sets.ml, iterate.ml, lists.ml and int.ml.
* Multivariate/metric.ml gains quotient topologies, the topology of
pointwise convergence, irreducible sets and sober spaces, with smaller
additions to topology.ml and canal.ml, and three matrix induction
theorems move from measure.ml to determinants.ml.
* 100/transcendence.ml now uses the general minimal_polynomial of
Library/fieldtheory.ml in place of its own.
There are also fixes so that files load the same way whatever was loaded
before them: explicit number priorities in many Multivariate and Library
files (with prioritize_complex() now calling prioritize_real() first),
type annotations in a few proofs, renamed bindings that used to hide
like-named theorems or tactics in other files, and renamed bound
variables sigma and tau that clashed with the constants of
Library/multiplicative.ml. A few existing theorems are restated in more
general or slightly different forms. New definitions:
algebra_norm
algebra_trace
basis_coordinates
basis_discriminant
extension_degree
field_of_fractions
finite_galois_subfields
fixed_field
fraction_field_map
free_basis
galois_extension
galois_group
group_cosets
inseparable_degree
inverse_limit_group
irreducible_in
jacobson_radical
localization_map
minimal_polynomial
minimal_prime_ideal
minimal_prime_over
mul_matrix
normal_extension
perfect_field
pointwise_topology
poly_discriminant
poly_resultant
poly_separable
poly_splits
poly_splits_over
projective_basis
purely_inseparable_extension
quotient_topology
radical_element
radical_extension
radical_number
residue_field
residue_hom
restricted_product_group
restricted_product_ring
ring_additive_group
ring_charpoly
ring_cofactor
ring_det
ring_homomorphism_extensions
ring_sign
separable_closure
separable_degree
separable_element
separable_extension
sober_space
splitting_extension
unit_group
and theorems:
ABELIAN_GALOIS_GROUP_FINITE_FIELD
ABELIAN_GALOIS_GROUP_ON_GENERATORS
ABELIAN_GALOIS_GROUP_RADICAL
ABELIAN_GALOIS_GROUP_ROOT_OF_UNITY
ABELIAN_GROUP_DIV_DIV
ABELIAN_GROUP_DIV_EQ
ABELIAN_GROUP_DIV_EQ_DIV
ABELIAN_GROUP_DIV_LCANCEL
ABELIAN_GROUP_MUL_CANCEL_LEMMA
ABELIAN_GROUP_MUL_DIV_CANCEL
ABELIAN_GROUP_MUL_SOLVE
ABELIAN_GROUP_SUM_SUM_PRODUCT
ABELIAN_GROUP_SUM_SWAP
ABELIAN_RESTRICTED_PRODUCT_GROUP
ABELIAN_RING_ADDITIVE_GROUP
ABELIAN_UNIT_GROUP
ALGEBRAICALLY_CLOSED_FIELD_COMPLEX_RING
ALGEBRAICALLY_CLOSED_FIELD_EQ_POLY_SPLITS
ALGEBRAICALLY_CLOSED_FIELD_EQ_POLY_SPLITS_ALT
ALGEBRAICALLY_CLOSED_FIELD_FINITE_SUBFIELD
ALGEBRAICALLY_CLOSED_FIELD_IMP_PERFECT
ALGEBRAICALLY_CLOSED_FIELD_NTH_ROOT
ALGEBRAICALLY_CLOSED_FIELD_POLY_SPLITS
ALGEBRAICALLY_CLOSED_FIELD_PRIMITIVE_ROOT_OF_UNITY
ALGEBRAICALLY_CLOSED_FIELD_ROOTS_OF_UNITY_IMAGE
ALGEBRAICALLY_CLOSED_FIELD_SINGLE_ROOT
ALGEBRAICALLY_CLOSED_IMP_NORMAL_EXTENSION
ALGEBRAIC_CLOSURE_EXISTS_BIGENOUGH
ALGEBRAIC_CLOSURE_EXTEND_HOMOMORPHISM_ROOT
ALGEBRAIC_OVER_EXISTS_MONIC_IRREDUCIBLE
ALGEBRAIC_OVER_POW_EQ
ALGEBRAIC_OVER_QINC_COMPLEX
ALGEBRA_NORM_0
ALGEBRA_NORM_0_FREE_BASIS
ALGEBRA_NORM_0_PROJECTIVE
ALGEBRA_NORM_1
ALGEBRA_NORM_EQ_0
ALGEBRA_NORM_EQ_0_FREE_BASIS
ALGEBRA_NORM_FIBRE_FINITE
ALGEBRA_NORM_FINITE_FIELD_POW
ALGEBRA_NORM_FREE_BASIS
ALGEBRA_NORM_INV
ALGEBRA_NORM_MINIMAL_POLYNOMIAL
ALGEBRA_NORM_MUL
ALGEBRA_NORM_POW
ALGEBRA_NORM_PRODUCT
ALGEBRA_NORM_PROJECTIVE_BASIS
ALGEBRA_NORM_PROJECTIVE_BASIS_ALT
ALGEBRA_NORM_SUBRING
ALGEBRA_NORM_SUB_CHARPOLY
ALGEBRA_NORM_SURJECTIVE_FINITE
ALGEBRA_NORM_UNIT
ALGEBRA_NORM_UNIT_PROJECTIVE
ALGEBRA_TRACE_0
ALGEBRA_TRACE_ADD
ALGEBRA_TRACE_FIBRE_FINITE
ALGEBRA_TRACE_FREE_BASIS
ALGEBRA_TRACE_LINCOMB_MUL
ALGEBRA_TRACE_MINIMAL_POLYNOMIAL
ALGEBRA_TRACE_MUL_LINCOMB
ALGEBRA_TRACE_NEG
ALGEBRA_TRACE_NILPOTENT
ALGEBRA_TRACE_NORM_BASE
ALGEBRA_TRACE_NORM_BASE_FREE_BASIS
ALGEBRA_TRACE_NORM_EMBEDDINGS
ALGEBRA_TRACE_NORM_EMBEDDINGS_GEN
ALGEBRA_TRACE_NORM_EMBEDDINGS_SEPARABLE
ALGEBRA_TRACE_NORM_EQ_IMAGE
ALGEBRA_TRACE_NORM_FINITE_FIELD
ALGEBRA_TRACE_NORM_GALOIS
ALGEBRA_TRACE_NORM_HOMOMORPHIC_IMAGE
ALGEBRA_TRACE_NORM_HOMOMORPHIC_IMAGE_PROJECTIVE
ALGEBRA_TRACE_NORM_INTERMEDIATE
ALGEBRA_TRACE_NORM_INTERMEDIATE_FREE_BASIS
ALGEBRA_TRACE_NORM_IN_CARRIER
ALGEBRA_TRACE_NORM_MINIMAL_POLYNOMIAL
ALGEBRA_TRACE_NORM_NO_PROJECTIVE_BASIS
ALGEBRA_TRACE_NORM_PROD_RING
ALGEBRA_TRACE_NORM_PURELY_INSEPARABLE
ALGEBRA_TRACE_NORM_SIMPLE
ALGEBRA_TRACE_NORM_TOWER
ALGEBRA_TRACE_PROJECTIVE_BASIS
ALGEBRA_TRACE_RING_SUM
ALGEBRA_TRACE_SCALAR
ALGEBRA_TRACE_SUB
ALGEBRA_TRACE_SUBRING
ALGEBRA_TRACE_SUM
ALGEBRA_TRACE_SURJECTIVE
ALGEBRA_TRACE_SURJECTIVE_FINITE
ALGEBRA_TRACE_TOWER_PROJECTIVE
ARTIN_FIXED_FIELD
ARTIN_SCHREIER_CYCLIC
ARTIN_SCHREIER_EXTENSION
ARTIN_SCHREIER_EXTENSION_EQ
BASIS_COORDINATES
BASIS_COORDINATES_0
BASIS_COORDINATES_ADD
BASIS_COORDINATES_BASIS
BASIS_COORDINATES_CHANGE_OF_BASIS
BASIS_COORDINATES_CHANGE_OF_BASIS_INVERSE
BASIS_COORDINATES_EQ
BASIS_COORDINATES_EXPAND
BASIS_COORDINATES_HOMOMORPHIC_IMAGE
BASIS_COORDINATES_IN_CARRIER
BASIS_COORDINATES_LINCOMB
BASIS_COORDINATES_LMUL
BASIS_COORDINATES_MUL
BASIS_COORDINATES_OUTSIDE
BASIS_COORDINATES_SUM
BASIS_COORDINATES_TRANS
BASIS_COORDINATES_UNIQUE
BASIS_DISCRIMINANT_CHANGE_OF_BASIS
BASIS_DISCRIMINANT_DEGENERATE
BASIS_DISCRIMINANT_EQ_0
BASIS_DISCRIMINANT_HOMOMORPHIC_IMAGE
BASIS_DISCRIMINANT_NILPOTENT
BASIS_DISCRIMINANT_NONZERO
BASIS_DISCRIMINANT_TIMES_COORD
CARD_EQ_FIBRES_HAS_SIZE
CARD_EQ_GROUP_COSETS_IMAGE_PREIMAGE
CARD_EQ_GROUP_COSETS_PREIMAGE
CARD_EQ_GROUP_COSETS_QUOTIENT_GROUP
CARD_EQ_LEFT_COSETS_GROUP_COSETS
CARD_EQ_RING_HOMOMORPHISM_EXTENSIONS
CARD_EXTENSION_DEGREE
CARD_GALOIS_GROUP_LE
CARD_GALOIS_GROUP_LE_SEPARABLE_DEGREE
CARD_RING_HOMOMORPHISM_EXTENSIONS_LE
CARTESIAN_PRODUCT_SUBGROUP_OF_RESTRICTED_PRODUCT_GROUP
CARTESIAN_PRODUCT_SUBRING_OF_RESTRICTED_PRODUCT_RING
CLOSED_IN_POINTWISE_PRODUCT
CLOSED_IN_POINTWISE_TOPOLOGY_AGREE
CLOSED_IN_QUOTIENT_TOPOLOGY
CLOSURE_OF_POINTWISE_TOPOLOGY
COEFF_0_1_RING_PRODUCT
COEFF_1_RING_DET
COEFF_1_RING_PRODUCT_PERMUTES
COEFF_POLY_CONST_MUL_VAR_MUL
COEFF_POLY_CONST_MUL_VAR_POW
COEFF_POLY_MUL_LE
COEFF_POLY_MUL_MONIC_SUBLEADING
COEFF_POLY_POW_X_MINUS_A_SUBLEADING
COEFF_RING_PRODUCT_LE
COEFF_RING_PRODUCT_MONIC_SUBLEADING
COEFF_RING_PRODUCT_X_MINUS
COEFF_RING_SUM_MONOMIALS
COEFF_RING_SUM_VARPOW_REV
COMPATIBLE_RIGHT_COSETS
COMPATIBLE_SEQUENCE_DIV
COMPLEX_RING_CHAR
COMPLEX_RING_CLAUSES
COMPLEX_RING_INV
COMPLEX_RING_OF_INT
COMPLEX_RING_OF_NUM
COMPLEX_RING_POW
COMPLEX_RING_SUM
COMPLEX_ROOTS_IRREDUCIBLE
CONTINUOUS_MAP_COMPLEX_INV
CONTINUOUS_MAP_FROM_QUOTIENT_TOPOLOGY
CONTINUOUS_MAP_INTO_DISCRETE_TOPOLOGY
CONTINUOUS_MAP_INTO_DISCRETE_TOPOLOGY_FIBRES
CONTINUOUS_MAP_LOCALLY_CONSTANT
CONTINUOUS_MAP_NORM
CONTINUOUS_MAP_POINTWISE_ACTION
CONTINUOUS_MAP_POINTWISE_EVALUATION
CONTINUOUS_MAP_POINTWISE_TOPOLOGY
CONTINUOUS_MAP_PROD_TOPOLOGY_ID
CONTINUOUS_MAP_QUOTIENT_TOPOLOGY
CYCLIC_GALOIS_GROUP_FINITE_FIELD
CYCLIC_GALOIS_GROUP_RADICAL
CYCLIC_GALOIS_GROUP_TRANSLATION
CYCLOTOMIC_EXTENSION_ABELIAN
CYCLOTOMIC_EXTENSION_ABELIAN_INTERMEDIATE
CYCLOTOMIC_GALOIS_GROUP_MODMUL
CYCLOTOMIC_GALOIS_GROUP_MODMUL_ISOMORPHISM
EVENPERM_GROUP_POW
EXTENSION_DEGREE_EQ_0
EXTENSION_DEGREE_EQ_1
EXTENSION_DEGREE_EQ_CARD_BASIS
EXTENSION_DEGREE_EQ_IMAGE
EXTENSION_DEGREE_EQ_TOWER
EXTENSION_DEGREE_ISOMORPHISM
EXTENSION_DEGREE_LE_INDEPENDENT_BOUND
EXTENSION_DEGREE_REFL
EXTENSION_DEGREE_SEPARABLE_INSEPARABLE
EXTENSION_DEGREE_SIMPLE
EXTENSION_DEGREE_SUBFIELD_GENERATED_DIVIDES
EXTENSION_DEGREE_TOWER_LAW
EXTENSION_LINCOMB_ADD
EXTENSION_LINCOMB_LMUL
EXTENSION_LINCOMB_MUL
EXTENSION_LINCOMB_SUM
EXTENSION_MUL_LINCOMB
FIELD_CHARPOLY_INTERMEDIATE
FIELD_CHARPOLY_MINIMAL_POLYNOMIAL
FIELD_CHARPOLY_SIMPLE
FIELD_COMPLEX_RING
FIELD_EXTENSION_FRACTION_RING_INTEGER_RING
FIELD_EXTENSION_FROM_SUBFIELD_GENERATED
FIELD_EXTENSION_IMP_SUBSET_I
FIELD_EXTENSION_INTO_INTERMEDIATE
FIELD_EXTENSION_QINC_COMPLEX
FIELD_EXTENSION_SUBFIELD_GENERATED
FIELD_EXTENSION_SUBRING_GENERATED_FINITE
FIELD_NONZERO_NONINVOLUTION
FIELD_OF_FRACTIONS_COMMON_DENOMINATOR
FIELD_OF_FRACTIONS_EQ
FIELD_OF_FRACTIONS_FRACTION_RING
FIELD_OF_FRACTIONS_IMP_INTEGRAL_DOMAIN
FIELD_OF_FRACTIONS_ISOMORPHISM_LEFT
FIELD_OF_FRACTIONS_ISOMORPHISM_RIGHT
FIELD_OF_FRACTIONS_PROPORTIONAL
FIELD_OF_FRACTIONS_RESIDUE_FIELD
FIELD_POLY_DEG_EQ_0
FIELD_PRIME_IDEAL_ZERO
FIELD_PRIME_IDEAL_ZERO_EXISTS
FIELD_RESIDUE_FIELD
FIELD_UNIT_GROUP
FINITELY_GENERATED_ABELIAN_GROUP_EXPONENTS
FINITE_ASSOCIATE_REPRESENTATIVES
FINITE_CYCLIC_GROUP_POWERS
FINITE_EXTENSION_EQ_IMAGE
FINITE_EXTENSION_FREE_BASIS
FINITE_EXTENSION_HOMOMORPHIC_IMAGE
FINITE_EXTENSION_NORMAL_CLOSURE
FINITE_EXTENSION_SUBFIELD_GENERATED
FINITE_EXTENSION_SUBFIELD_GENERATORS
FINITE_FIBRES_BIJECTIONS
FINITE_FIELD_ALGEBRAIC_CLOSURE_LAYER
FINITE_FIELD_CARD_GE_2
FINITE_FIELD_CARD_ROOTS_OF_UNITY
FINITE_FIELD_CYCLIC_UNIT_GROUP
FINITE_FIELD_EXISTS
FINITE_FIELD_EXISTS_GEN
FINITE_FIELD_EXTENSION_EXISTS
FINITE_FIELD_GALOIS_EXTENSION
FINITE_FIELD_HOMOMORPHISM_EXISTS
FINITE_FIELD_HOMOMORPHISM_IMAGE
FINITE_FIELD_IMP_PERFECT
FINITE_FIELD_INTERMEDIATE_FIELDS
FINITE_FIELD_INTERMEDIATE_FIELD_DIVISOR
FINITE_FIELD_INTERMEDIATE_FIELD_EXPLICIT
FINITE_FIELD_IRREDUCIBLE_COUNT
FINITE_FIELD_IRREDUCIBLE_EXISTS
FINITE_FIELD_IRREDUCIBLE_ROOTS
FINITE_FIELD_IRREDUCIBLE_ROOT_EXISTS
FINITE_FIELD_IRREDUCIBLE_ROOT_POW
FINITE_FIELD_LAYERS_COVER
FINITE_FIELD_LAYER_POW
FINITE_FIELD_NORMAL_IMP_GALOIS
FINITE_FIELD_POW_CARD_EXP
FINITE_FIELD_PRIMITIVE_ELEMENT
FINITE_FIELD_PRIMITIVE_ROOT
FINITE_FIELD_ROOTS_OF_UNITY
FINITE_FIELD_SPLITTING_EXTENSION
FINITE_FIELD_SUBFIELD_CARD
FINITE_GALOIS_GROUP
FINITE_GALOIS_SUBFIELDS_ELEMENT
FINITE_GALOIS_SUBFIELDS_FINITE
FINITE_GALOIS_SUBFIELDS_FINITE_FIELD
FINITE_GALOIS_SUBFIELDS_UPPER_BOUND
FINITE_GALOIS_SUBFIELDS_UPPER_BOUNDS
FINITE_GALOIS_SUBFIELD_RESTRICTION_EQ
FINITE_GROUP_COSETS
FINITE_GROUP_HOMOMORPHISMS_KERNEL
FINITE_IDEALS_SUPERSET
FINITE_INTEGRAL_DOMAIN_CYCLIC
FINITE_INTEGRAL_DOMAIN_POW_CARD
FINITE_INTEGRAL_DOMAIN_POW_CARD_SUB_1
FINITE_INTEGRAL_DOMAIN_UNIT
FINITE_IN_COMPACT_IMP_CLOSED_DISCRETE
FINITE_MONOMIALS_DEG_LT
FINITE_POLY_DEG_LE
FINITE_PROPER_PREFIXES
FINITE_RING_MULTSYS_CYCLIC
FINITE_RING_REGULAR
FINITE_SUBFIELD_EXPLICIT
FIRST_GROUP_EPIMORPHISM_THEOREM_EXPLICIT
FIRST_GROUP_ISOMORPHISM_THEOREM_EXPLICIT
FIXED_FIELD_ANTIMONO
FIXED_FIELD_ANTIMONO_EQ
FIXED_FIELD_CONJUGATE
FIXED_FIELD_EMPTY
FIXED_FIELD_GALOIS_GROUP
FIXED_FIELD_GALOIS_GROUP_GENERATORS
FIXED_FIELD_GALOIS_GROUP_INTERMEDIATE
FIXED_FIELD_GALOIS_SUBSET
FIXED_FIELD_INTER
FIXED_FIELD_SUBGROUP_GENERATED
FIXED_FIELD_SUBSET
FIXED_FIELD_UNION
FRACTION_FIELD_COMMON_DENOMINATOR
FRACTION_FIELD_MAP
FRACTION_FIELD_MAP_EQ
FRACTION_FIELD_MAP_ISOMORPHISM
FREE_BASES_SIZE_EQ
FREE_BASIS_DELTA
FREE_BASIS_EQ_IMAGE
FREE_BASIS_EXISTS
FREE_BASIS_EXTENSION_DEGREE
FREE_BASIS_FIELD
FREE_BASIS_FROM_RING_BASIS
FREE_BASIS_HAS_SIZE
FREE_BASIS_IMP_ALGEBRAIC
FREE_BASIS_IMP_FINITE_EXTENSION
FREE_BASIS_INDEPENDENT
FREE_BASIS_INDEPENDENT_EQ
FREE_BASIS_IN_CARRIER
FREE_BASIS_MONOMORPHISM
FREE_BASIS_PROJECTIVE
FREE_BASIS_QUOTIENT_RING_PRINCIPAL
FREE_BASIS_RING_DIVIDES
FREE_BASIS_RING_SUM_IMAGE
FREE_BASIS_SIMPLE_EXTENSION
FREE_BASIS_SPANNING_DEGREE
FREE_BASIS_SPANNING_EQ
FREE_BASIS_TRANS
FREE_BASIS_UNIQUE
FROBENIUS_ADD_POWER
FROBENIUS_SUM_POWER
FUNDAMENTAL_THEOREM_OF_GALOIS_THEORY
GALOIS_COMPOSITUM
GALOIS_COMPOSITUM_DEGREE
GALOIS_COMPOSITUM_DISJOINT
GALOIS_COMPOSITUM_MONOMORPHISM
GALOIS_COMPOSITUM_PROD_GROUP
GALOIS_COMPOSITUM_PROD_GROUP_MONOMORPHISM
GALOIS_COMPOSITUM_SOLVABLE
GALOIS_CORRESPONDENCE
GALOIS_CORRESPONDENCE_DEGREE
GALOIS_CORRESPONDENCE_INDEX
GALOIS_CORRESPONDENCE_NORMAL
GALOIS_EXTENSION_ARTIN_SCHREIER
GALOIS_EXTENSION_COMPOSITUM
GALOIS_EXTENSION_DISTINCT_ROOTS
GALOIS_EXTENSION_EQ_CARD
GALOIS_EXTENSION_EQ_FIXED_FIELD
GALOIS_EXTENSION_EQ_SEPARABLE_SPLITTING
GALOIS_EXTENSION_GENERATORS_EQ
GALOIS_EXTENSION_HOMOMORPHIC_IMAGE
GALOIS_EXTENSION_INTERMEDIATE
GALOIS_EXTENSION_ISOMORPHISM
GALOIS_EXTENSION_LIFT
GALOIS_EXTENSION_NORMAL_SUBGROUP
GALOIS_EXTENSION_REFL
GALOIS_EXTENSION_SIMPLE_CYCLIC_EQ
GALOIS_EXTENSION_SIMPLE_EQ
GALOIS_EXTENSION_SUBFIELD_GENERATED
GALOIS_GROUP
GALOIS_GROUP_ACTION
GALOIS_GROUP_ACTION_ON_ROOTS
GALOIS_GROUP_ACTION_ON_ROOTS_TRANSITIVE
GALOIS_GROUP_ANTIMONO
GALOIS_GROUP_ANTIMONO_EQ
GALOIS_GROUP_ARTIN_SCHREIER
GALOIS_GROUP_BIJ_RING_HOMOMORPHISM_EXTENSIONS
GALOIS_GROUP_BIJ_RING_HOMOMORPHISM_EXTENSIONS_GEN
GALOIS_GROUP_BIJ_RING_HOMOMORPHISM_EXTENSIONS_NORMAL
GALOIS_GROUP_CARD_ROOTS_DIVIDES
GALOIS_GROUP_COMPOSE
GALOIS_GROUP_COMPOSITUM
GALOIS_GROUP_CONJUGATE
GALOIS_GROUP_CUBIC
GALOIS_GROUP_DISCRIMINANT_SQUARE_ROOT
GALOIS_GROUP_EQ_IMAGE
GALOIS_GROUP_EQ_ON_GENERATORS
GALOIS_GROUP_EVEN_EQ_DISCRIMINANT_SQUARE
GALOIS_GROUP_EXTEND_HOMOMORPHISM
GALOIS_GROUP_FINITE_FIELD
GALOIS_GROUP_FINITE_FIELD_EXPONENT
GALOIS_GROUP_FIXED_FIELD
GALOIS_GROUP_FIXES
GALOIS_GROUP_FROBENIUS
GALOIS_GROUP_I
GALOIS_GROUP_IMAGE_INVERSE
GALOIS_GROUP_IMAGE_NORMAL_INTERMEDIATE
GALOIS_GROUP_IMAGE_ROOTS
GALOIS_GROUP_INDEPENDENT
GALOIS_GROUP_INTER
GALOIS_GROUP_INTERMEDIATE_NORMAL_SUBGROUP
GALOIS_GROUP_INTERMEDIATE_SUBGROUP
GALOIS_GROUP_INTERMEDIATE_SUBGROUP_GENERATED
GALOIS_GROUP_INVERSE
GALOIS_GROUP_IN_CARRIER
GALOIS_GROUP_KUMMER_ROOT_OF_UNITY
GALOIS_GROUP_LOCAL
GALOIS_GROUP_ORBIT
GALOIS_GROUP_ORBIT_FINITE
GALOIS_GROUP_PERMUTES
GALOIS_GROUP_POLY_EVAL
GALOIS_GROUP_POW_ADD_FIXED
GALOIS_GROUP_POW_MUL_FIXED
GALOIS_GROUP_POW_RING_POW
GALOIS_GROUP_PRIME_TRANSPOSITION
GALOIS_GROUP_PRIME_TRANSPOSITION_EXPLICIT
GALOIS_GROUP_QUOTIENT
GALOIS_GROUP_RESTRICT
GALOIS_GROUP_RESTRICTION
GALOIS_GROUP_RESTRICTION_HOMOMORPHISM
GALOIS_GROUP_RESTRICTION_NORMAL
GALOIS_GROUP_RING_AUTOMORPHISM
GALOIS_GROUP_RING_HOMOMORPHISM
GALOIS_GROUP_RING_MONOMORPHISM
GALOIS_GROUP_SUBFIELD_GENERATED_IMAGE
GALOIS_GROUP_SUBGROUP
GALOIS_GROUP_TRANSITIVE_ON_ROOTS
GALOIS_GROUP_VANDERMONDE_ROOTS
GALOIS_IMP_ALGEBRAIC_EXTENSION
GALOIS_IMP_FIELD_EXTENSION
GALOIS_IMP_NORMAL_EXTENSION
GALOIS_IMP_SEPARABLE_EXTENSION
GALOIS_PRODUCT_BASE
GALOIS_PRODUCT_CONJUGATE
GALOIS_PRODUCT_EQ_0
GALOIS_PRODUCT_IN_BASE
GALOIS_PRODUCT_IN_FIXED_FIELD
GALOIS_PRODUCT_MUL
GALOIS_SOLVABLE_EQ_RADICAL
GALOIS_SUM_ADD
GALOIS_SUM_EQ_1_EXISTS
GROUP_COSETS_AS_IMAGE
GROUP_COSETS_LEFT_COSETS
GROUP_HOMOMORPHISMS_UNITS_INDEPENDENT
GROUP_HOMOMORPHISMS_UNITS_INDEPENDENT_LEMMA
GROUP_HOMOMORPHISMS_UNITS_INDEPENDENT_SET
GROUP_HOMOMORPHISM_EPIMORPHISM_FACTOR
GROUP_HOMOMORPHISM_INTEGER_MOD_GROUP_REM
GROUP_HOMOMORPHISM_RESTRICTED_PRODUCT
GROUP_HOMOMORPHISM_RESTRICTED_PRODUCT_COMPONENTWISE
GROUP_HOMOMORPHISM_RESTRICTED_PRODUCT_INJECTION
GROUP_HOMOMORPHISM_RESTRICTED_PRODUCT_PROJECTION
GROUP_HOMOMORPHISM_RESTRICTION
GROUP_HOMOMORPHISM_RING_ADDITIVE_GROUP
GROUP_HOMOMORPHISM_UNIT_GROUP
GROUP_ISOMORPHISM_INVERSE_LIMIT_GROUP
GROUP_ORDER_12_NORMAL_SUBGROUP
GROUP_ORDER_6_NORMAL_SUBGROUP
GROUP_POW_PERIODIC
GROUP_POW_RESTRICTED_PRODUCT_GROUP
GROUP_PREIMAGE_IMAGE_PREIMAGE
GROUP_SETMUL_CARRIER_SUBGROUP
GROUP_SETMUL_IMAGE_RIGHT_COSET
GROUP_SETMUL_RIGHT_COSET_BETWEEN
GROUP_SETMUL_SWAP
GROUP_SUM_HOMOMORPHIC_IMAGE
GROUP_SUM_RING_ADDITIVE_GROUP
GROUP_SUM_SUM_GROUP_COMPONENT
GROUP_SUM_SUM_GROUP_INJECTIONS
GROUP_ZPOW_RESTRICTED_PRODUCT_GROUP
HAS_REAL_DERIVATIVE_QUINTIC
HAS_SIZE_GROUP_COSETS
HAS_SIZE_POLY_DEG_LT
HAS_SIZE_RING_HOMOMORPHISM_EXTENSIONS
HAS_SIZE_SEPARABLE_DEGREE
HAUSDORFF_SPACE_POINTWISE_TOPOLOGY
HILBERT_90
HILBERT_90_ADDITIVE
HILBERT_90_ADDITIVE_CYCLIC
HILBERT_90_ADDITIVE_CYCLIC_EQ
HILBERT_90_ADDITIVE_FINITE_FIELD
HILBERT_90_CYCLIC
HILBERT_90_CYCLIC_EQ
HILBERT_90_FINITE_FIELD
HOMEOMORPHIC_MAP_QUOTIENT_TOPOLOGY
HOMOGENEOUS_SYSTEM_NONTRIVIAL_SOLUTION
IDEAL_GENERATED_ADJOIN_EXPLICIT
IDEAL_GENERATED_ADJOIN_INV
IDEAL_GENERATED_POLY_POINT
IDEAL_GENERATED_UNIT_FIELD_TEST
IMAGE_SUBSET_FIXED_FIELD_GALOIS_GROUP
INJECTIVE_ON_COMMUTING_SQUARE
INSEPARABLE_DEGREE_CHAR_POWER
INSEPARABLE_DEGREE_EQ_1
INSEPARABLE_DEGREE_TOWER
INTEGER_MOD_RING_CARRIER_REM_EQ
INTEGER_RING_PRODUCT
INTEGER_RING_SUM
INTEGRAL_DOMAIN_ORDER_DIVIDES_MAXIMAL
INTEGRAL_DOMAIN_ORDER_NONZERO
INTEGRAL_DOMAIN_ROOTS_OF_UNITY_CYCLIC
INTEGRAL_DOMAIN_SQUARE_EQ
INVERSE_LIMIT_GROUP
INVERSE_LIMIT_SUBGROUP_OF_PRODUCT_GROUP
IN_CROSS_FST_SND
IN_FINITE_GALOIS_SUBFIELDS
IN_FIXED_FIELD
IN_GALOIS_GROUP
IN_GALOIS_GROUP_INTERMEDIATE
IN_GALOIS_GROUP_SUBFIELD_GENERATED
IN_GROUP_COSETS
IN_GROUP_SETMUL
IN_IDEAL_GENERATED_INSERT_IDEAL
IN_IDEAL_GENERATED_POLY_CONST
IN_JACOBSON_RADICAL
IN_NILRADICAL
IN_RADICAL_MINIMAL_PRIMES
IN_RADICAL_PRIME_IDEALS
IN_RIGHT_COSET_TRANS
IN_RING_IDEAL_SUB_ADD
IN_RING_IDEAL_SUB_MUL
IN_RING_KERNEL_SUB
IN_SEPARABLE_CLOSURE
IRREDUCIBLE_DIVIDES_X_POW_SUB_X
IRREDUCIBLE_IMP_CONNECTED_IN
IRREDUCIBLE_IN_CLOSURE_OF
IRREDUCIBLE_IN_CONTINUOUS_MAP_IMAGE
IRREDUCIBLE_IN_SING
IRREDUCIBLE_ROOT_IMP_DEG_EQ_1
ISOMORPHIC_FINITE_FIELDS
ISOMORPHIC_GALOIS_GROUPS
ISOMORPHIC_GALOIS_GROUPS_SPLITTING
ISOMORPHIC_RING_PERFECT_FIELD
ITER_INTERTWINE_INVARIANT
IWASAWA_LEMMA
IWASAWA_SIMPLE
JACOBSON_RADICAL_EQ_INTERS_MAXIMAL_IDEALS
JACOBSON_RADICAL_LOCAL_RING
JACOBSON_RADICAL_SUBSET
KUMMER_CYCLIC_EXTENSION
KUMMER_CYCLIC_EXTENSION_EQ
KUMMER_EXTENSION_ABELIAN
KUMMER_EXTENSION_ABELIAN_INTERMEDIATE
KUMMER_EXTENSION_CYCLIC
KUMMER_EXTENSION_CYCLIC_INTERMEDIATE
KUMMER_ROOTS_SEPARABLY_CLOSED
LAGRANGE_THEOREM_GROUP_COSETS
LINEAR_POLY_ASSOCIATE_X_MINUS_A
LIST_SNOC_EXISTS
LOCALIZATION_MAP
LOCALIZATION_MAP_COMPOSE
LOCALIZATION_MAP_I
LOCALLY_COMPACT_SPACE_EUCLIDEAN
LOCAL_RING_JACOBSON_RADICAL
LOCAL_RING_MAXIMAL_IDEAL_NONUNITS
LOCAL_RING_PRIME_SUBSET_MAXIMAL
LOCAL_RING_PROPER_IDEAL_SUBSET_MAXIMAL
LOCAL_RING_SELECT_MAXIMAL_IDEAL
LOCAL_RING_UNIT_ADD_NONUNIT
MATROID_BASIS_LARGE_INDEPENDENT
MATROID_BASIS_SMALL_SPANNING
MATROID_DIMENSION_LE_INDEPENDENT_BOUND
MAXIMAL_IDEAL_EPIMORPHISM_KERNEL
MAXIMAL_IDEAL_LOCALIZATION_AT_PRIME
MAXIMAL_IDEAL_LOCALIZATION_AT_PRIME_CONTRACTION
MAXIMAL_IDEAL_POLY_POINT
MAXIMAL_IDEAL_POLY_RING_EPIMORPHISM
MINIMAL_POLYNOMIAL
MINIMAL_POLYNOMIAL_ASSOCIATES_IRREDUCIBLE
MINIMAL_POLYNOMIAL_COEFF_EMBEDDINGS
MINIMAL_POLYNOMIAL_DEG_DIVIDES_EXTENSION_DEGREE
MINIMAL_POLYNOMIAL_DEG_EQ_1
MINIMAL_POLYNOMIAL_DEG_EQ_CHAR
MINIMAL_POLYNOMIAL_DEG_LE
MINIMAL_POLYNOMIAL_DEG_LE_EXTENSION_DEGREE
MINIMAL_POLYNOMIAL_DIVIDES
MINIMAL_POLYNOMIAL_EMBEDDINGS
MINIMAL_POLYNOMIAL_EMBEDDING_DIVIDES
MINIMAL_POLYNOMIAL_FINITE_ORBIT
MINIMAL_POLYNOMIAL_IN_CARRIER
MINIMAL_POLYNOMIAL_IRREDUCIBLE
MINIMAL_POLYNOMIAL_MONIC
MINIMAL_POLYNOMIAL_MONOMORPHIC_IMAGE
MINIMAL_POLYNOMIAL_NONZERO
MINIMAL_POLYNOMIAL_POWERS_HAS_SIZE
MINIMAL_POLYNOMIAL_POWERS_INDEPENDENT
MINIMAL_POLYNOMIAL_QINC_COMPLEX
MINIMAL_POLYNOMIAL_ROOTS_IRREDUCIBLE
MINIMAL_POLYNOMIAL_SUBRING_GENERATED
MINIMAL_POLYNOMIAL_UNIQUE
MINIMAL_POLYNOMIAL_VANISHES
MINIMAL_POLYNOMIAL_VANISHES_HOMOMORPHIC_IMAGE
MINIMAL_PRIME_IDEAL_EXISTS
MINIMAL_PRIME_IDEAL_OVER
MINIMAL_PRIME_OVER_EXISTS
MINIMAL_PRIME_OVER_GENERATED
MINIMAL_PRIME_OVER_LOCAL_RADICAL
MINIMAL_PRIME_OVER_POW
MINIMAL_PRIME_OVER_PRINCIPAL
MONIC_ASSOCIATE_EXISTS
MONIC_DIVIDES_EQ
MONIC_EPIMORPHIC_PREIMAGE
MONIC_EQ_X_MINUS_A
MONIC_FACTOR_COEFFS_PRIME_IDEAL
MONIC_HOMOMORPHIC_IMAGE
MONIC_POLY_ADD_LOWER
MONIC_POLY_EQ_ROOTS_PRODUCT
MONIC_POLY_EXTEND_WEIGHT
MONIC_POLY_SPLIT
MONIC_SUBFIELD_GENERATED
MONIC_UNIT_EQ_DEG_0
MONIC_VAR_POW_SUB_VAR
MONIC_X_MINUS_A
MUL_MATRIX_0
MUL_MATRIX_1
MUL_MATRIX_ADD
MUL_MATRIX_CHANGE_OF_BASIS
MUL_MATRIX_CHARPOLY_BASIS
MUL_MATRIX_CHARPOLY_INTERMEDIATE
MUL_MATRIX_CHARPOLY_ROOT
MUL_MATRIX_EXPAND
MUL_MATRIX_HOMOMORPHIC_IMAGE
MUL_MATRIX_IN_CARRIER
MUL_MATRIX_LMUL
MUL_MATRIX_MUL
MUL_MATRIX_POLY_MUL
MUL_MATRIX_RING_SUM
MUL_MATRIX_SCALAR
MUL_MATRIX_SUBRING
MUL_MATRIX_TRANS
NILRADICAL_EQ_INTERS_MINIMAL_PRIMES
NILRADICAL_LOCALIZATION
NILRADICAL_SUBSET
NILRADICAL_SUBSET_JACOBSON_RADICAL
NORMAL_EXTENSION_COMPOSITUM
NORMAL_EXTENSION_EQ_CARD_GALOIS_GROUP
NORMAL_EXTENSION_EQ_EMBEDDINGS
NORMAL_EXTENSION_EQ_GALOIS_STABLE
NORMAL_EXTENSION_EQ_MINIMAL_POLYNOMIALS_SPLIT
NORMAL_EXTENSION_GENERATED_BY_ROOTS
NORMAL_EXTENSION_I
NORMAL_EXTENSION_IMAGES_EQ
NORMAL_EXTENSION_INTERMEDIATE
NORMAL_EXTENSION_ISOMORPHIC_IMAGE
NORMAL_EXTENSION_ISOMORPHISM
NORMAL_EXTENSION_REFL
NORMAL_IMP_ALGEBRAIC_EXTENSION
NORMAL_IMP_FIELD_EXTENSION
NORMAL_SUBGROUP_INTER_SUBGROUP_GENERATED
NORMAL_SUBGROUP_QUOTIENT_GROUP_IMAGE
NOT_RADICAL_QUINTIC_ROOT
NOT_RADICAL_ROOT_RATIONAL
NOT_RADICAL_ROOT_REAL_FIELD
NOT_SOLVABLE_IMP_NO_RADICAL_ROOT
NSUM_DIGITS_BOUND
NSUM_DIGITS_UNIQUE
NSUM_LE_CARD_DELETE
NSUM_NUMSEG_LAST
NSUM_NUMSEG_MONO
OPEN_IN_POINTWISE_PRODUCT_AGREE
OPEN_IN_POINTWISE_TOPOLOGY_AGREE
OPEN_IN_POINTWISE_TOPOLOGY_POINT
OPEN_IN_QUOTIENT_TOPOLOGY
OPEN_IN_QUOTIENT_TOPOLOGY_INJ
PERFECT_FIELD_CHAR_0
PERFECT_FIELD_EPIMORPHIC_IMAGE
PERFECT_FIELD_EQ_FROBENIUS_AUTOMORPHISM
PERFECT_FIELD_EQ_FROBENIUS_AUTOMORPHISM_GEN
PERFECT_FIELD_EQ_IRREDUCIBLE_DERIV_NONZERO
PERFECT_FIELD_EQ_SEPARABLE_IRREDUCIBLES
PERFECT_FIELD_IMP_FIELD
PERFECT_FIELD_IMP_SEPARABLE
PERFECT_FIELD_IMP_SEPARABLE_ELEMENT
PERFECT_FIELD_IMP_SEPARABLE_EXTENSION
PERFECT_FIELD_ISOMORPHIC_IMAGE
PERFECT_FIELD_POLY_DERIV_EQ_0
PERFECT_FIELD_SEPARABLE_EQ_SQUAREFREE
PERMUTES
PERMUTES_CNJ
PERMUTES_DOUBLETON
PERMUTES_EQ
PERMUTES_INJECTIVE_RESTRICT
PID_COPRIME_PRIME_POWERS
PID_DIVIDES_PRIME_POWERS
POINTWISE_PRODUCT_NEIGHBOURHOOD
POINTWISE_TOPOLOGY_NEIGHBOURHOOD
POLY_COMPOSE_HOMOMORPHISM_X_MINUS_POW
POLY_DEG_0_IMP_SPLITS
POLY_DEG_1_IMP_SPLITS
POLY_DEG_1_IMP_SPLITS_MONIC
POLY_DEG_2_IRREDUCIBLE
POLY_DEG_ADD_CONST
POLY_DEG_ASSOCIATES
POLY_DEG_CMUL_LE
POLY_DEG_CMUL_MONIC
POLY_DEG_CONST_VARPOW_LE
POLY_DEG_LMUL_MONIC
POLY_DEG_POW_MONIC
POLY_DEG_PRODUCT_MONIC
POLY_DEG_PRODUCT_POW_MONIC
POLY_DEG_RING_PRODUCT_LE
POLY_DEG_RING_PRODUCT_X_MINUS_LE
POLY_DEG_RING_SUM_VARPOW_REV
POLY_DEG_RMUL_MONIC
POLY_DEG_SPLIT
POLY_DEG_SPLIT_MONIC
POLY_DEG_SUBFIELD_GENERATED
POLY_DEG_SUB_CONST
POLY_DEG_VAR_MINUS_A
POLY_DERIV_EQ_0_COEFF
POLY_DERIV_EQ_0_EXPLICIT
POLY_DERIV_VAR_POW_ZERO
POLY_DISCRIMINANT_CMUL
POLY_DISCRIMINANT_EQ_0
POLY_DISCRIMINANT_HOMOMORPHISM
POLY_DISCRIMINANT_IN_CARRIER
POLY_DISCRIMINANT_RESULTANT
POLY_DISCRIMINANT_ROOTS
POLY_DISCRIMINANT_SYLVESTER
POLY_DISCRIMINANT_VANDERMONDE
POLY_EQSET_BOUND
POLY_EVALUATE_SUB_IN_IDEAL
POLY_EVALUATE_TAYLOR
POLY_EVAL_COMPLEX_RING
POLY_EVAL_DERIV_RING_PRODUCT_X_MINUS
POLY_EVAL_RING_PRODUCT_EQ_0
POLY_EVAL_SPLIT
POLY_EVAL_SUBFIELD_GENERATED
POLY_EVAL_SUBRING_GENERATED
POLY_EVAL_VAR_POW_SUB_CONST
POLY_EVAL_VAR_POW_SUB_VAR
POLY_EXPAND_REV
POLY_EXTEND_COMPOSE_COEFFS
POLY_EXTEND_CONST_VARPOW
POLY_EXTEND_QINC_COMPLEX
POLY_EXTEND_VARPOW
POLY_INSEPARABLE_ROOTS_LT_DEG
POLY_IRREDUCIBLE_DIVIDES_DERIV_EQ
POLY_LEVELSET_BOUND
POLY_NONCONSTANT_IMP_NZ
POLY_PRODUCT_HOMOMORPHIC_IMAGE
POLY_RESULTANT_COMBINATION
POLY_RESULTANT_EQ_0
POLY_RESULTANT_HOMOMORPHISM
POLY_RESULTANT_IN_CARRIER
POLY_RESULTANT_LCONST
POLY_RESULTANT_RCONST
POLY_RESULTANT_ROOTS
POLY_RESULTANT_SYM
POLY_RESULTANT_X_MINUS
POLY_RESULTANT_X_MINUS_MUL
POLY_RING_MONOMORPHIC_PREIMAGE
POLY_ROOTS_MONOMORPHIC_IMAGE
POLY_ROOTS_SPLIT
POLY_ROOT_BOUND_EXTENSION
POLY_ROOT_COUNT_IMP_PRODUCT
POLY_ROOT_COUNT_IMP_SPLITS
POLY_ROOT_DECOMPOSE
POLY_SEPARABLE_DIVISOR
POLY_SEPARABLE_EQ_DERIV_NONZERO
POLY_SEPARABLE_FROM_MONOMORPHIC_IMAGE
POLY_SEPARABLE_MONOMORPHIC_IMAGE
POLY_SEPARABLE_ROOT_COUNT_EQ
POLY_SEPARABLE_ROOT_DERIV
POLY_SEPARABLE_VAR_POW_SUB_CONST
POLY_SEPARABLE_VAR_POW_SUB_VAR
POLY_SEPARABLE_X_MINUS_A
POLY_SPLITS
POLY_SPLITS_0
POLY_SPLITS_1
POLY_SPLITS_CASES
POLY_SPLITS_CASES_ALT
POLY_SPLITS_CONST
POLY_SPLITS_DIVISOR
POLY_SPLITS_EQ_IRREDUCIBLES
POLY_SPLITS_HAS_ROOT
POLY_SPLITS_HOMOMORPHIC_IMAGE
POLY_SPLITS_IN_CARRIER
POLY_SPLITS_IN_SUBRING
POLY_SPLITS_IN_SUBRING_MONIC
POLY_SPLITS_MONOMORPHIC_PREIMAGE
POLY_SPLITS_MUL
POLY_SPLITS_OVER_ALGEBRAICALLY_CLOSED_FIELD
POLY_SPLITS_OVER_DISTINCT_ROOTS
POLY_SPLITS_OVER_EQ_IRREDUCIBLES
POLY_SPLITS_OVER_EXPLICIT
POLY_SPLITS_OVER_EXTENSION
POLY_SPLITS_OVER_IRREDUCIBLE_ROOT_COUNT
POLY_SPLITS_OVER_SEPARABLE_ROOT_COUNT
POLY_SPLITS_OVER_SEPARABLE_ROOT_COUNT_EQ
POLY_SPLITS_OVER_SQUAREFREE_ROOT_COUNT
POLY_SPLITS_OVER_TRIVIAL_RING
POLY_SPLITS_PRODUCT
POLY_SPLITS_SQUAREFREE_ROOT_COUNT
POLY_SPLITS_SQUAREFREE_ROOT_COUNT_EXPLICIT
POLY_SPLITS_UNIT
POLY_SPLITS_VAR
POLY_SPLITS_X_MINUS_A
POLY_SUBRING_GENERATED_MUL
POLY_SUB_EVALUATE_IN_IDEAL_GENERATED
POLY_TOP_SPLIT
POLY_VAR_POW_SUB_CONST
POLY_VAR_POW_SUB_VAR
POLY_VAR_SUBRING_GENERATED
POWER_INJECTIVE_BELOW_MINPOLY_DEG
PRIME_3
PRIME_IDEAL_COLON_SING
PRIME_IDEAL_INTERS_CHAIN
PRIME_IDEAL_LOCALIZATION_CONTRACTION_EXTENSION
PRIME_IDEAL_LOCALIZATION_EXTENSION
PRIME_IDEAL_PRODUCT_RING
PRIME_IDEAL_PROD_RING
PRIME_IDEAL_QUOTIENT_RING_IMAGE
PRIME_IDEAL_RING_KERNEL
PRIME_IDEAL_UNIT_MUL
PRIME_SUBFIELD_HOMOMORPHISM_EXISTS
PRIME_SUBFIELD_MONOMORPHIC_IMAGE
PRIME_SUBFIELD_SUBFIELD
PRIME_SUBFIELD_SUBFIELD_GENERATED
PRIME_SUBFIELD_TOWER_LAW
PRIME_TRANSPOSITION_NO_RADICAL_ROOT
PRIME_TRANSPOSITION_NO_RADICAL_ROOT_SPLITS
PRIMITIVE_ELEMENT_EQ_SEPARATING_EMBEDDINGS
PRIMITIVE_ELEMENT_GENSET
PRIMITIVE_ELEMENT_INFINITE
PRIMITIVE_ELEMENT_THEOREM
PRIMITIVE_ELEMENT_THEOREM_EQ
PRIMITIVE_ELEMENT_TWO_GENERATORS
PRIMITIVE_ROOT_OF_UNITY_EXISTS
PROJECTIVE_BASIS_0
PROJECTIVE_BASIS_ADD
PROJECTIVE_BASIS_CHANGE
PROJECTIVE_BASIS_EQ_IMAGE
PROJECTIVE_BASIS_EXISTS_FIELD
PROJECTIVE_BASIS_EXPAND
PROJECTIVE_BASIS_IMP_FINITE_EXTENSION
PROJECTIVE_BASIS_IN_CARRIER
PROJECTIVE_BASIS_LINEAR
PROJECTIVE_BASIS_LMUL
PROJECTIVE_BASIS_MUL
PROJECTIVE_BASIS_NEG
PROJECTIVE_BASIS_PROD_RING
PROJECTIVE_BASIS_RING_SUM
PROJECTIVE_BASIS_SUB
PROJECTIVE_BASIS_SUM
PROJECTIVE_BASIS_TRANS
PROPER_IDEAL_LOCALIZATION_EQ
PURELY_INSEPARABLE_EXTENSION_DEGREE
PURELY_INSEPARABLE_EXTENSION_EQ_POW
PURELY_INSEPARABLE_EXTENSION_PERFECT
PURELY_INSEPARABLE_EXTENSION_TRANS
PURELY_INSEPARABLE_IMP_ALGEBRAIC_EXTENSION
PURELY_INSEPARABLE_IMP_FIELD_EXTENSION
PURELY_INSEPARABLE_OVER_FROBENIUS_IMAGE
PURELY_INSEPARABLE_OVER_SEPARABLE_CLOSURE
QUINTIC_AT_LEAST_3_REAL_ROOTS
QUINTIC_AT_MOST_3_REAL_ROOTS
QUINTIC_COMPLEX_REAL_ROOTS
QUINTIC_NONREAL_ROOTS
QUINTIC_RATIONAL_IRREDUCIBLE
QUINTIC_REAL_ROOTS
QUOTIENT_GROUP_BIJ
QUOTIENT_GROUP_CARRIER
QUOTIENT_GROUP_REPRESENTATIVE
QUOTIENT_GROUP_TRANSITION
QUOTIENT_MAP_QUOTIENT_TOPOLOGY
QUOTIENT_MAP_QUOTIENT_TOPOLOGY_EQ
QUOTIENT_POLY_RING_HAS_SIZE
QUOTIENT_RING_HOMOMORPHISM_EXISTS
QUOTIENT_RING_PREIMAGE_IDEAL_GENERATED
QUOTIENT_RING_PRIME_IDEAL_CORRESPONDENCE
QUOTIENT_RING_REDUCED
QUOTIENT_RING_ZERO_ISOMORPHIC
RADICAL_ELEMENTS_COMMON_RADICAL_EXTENSION
RADICAL_ELEMENT_ADD
RADICAL_ELEMENT_BASE
RADICAL_ELEMENT_DIV
RADICAL_ELEMENT_HOMOMORPHIC_IMAGE
RADICAL_ELEMENT_INV
RADICAL_ELEMENT_IN_CARRIER
RADICAL_ELEMENT_MUL
RADICAL_ELEMENT_NEG
RADICAL_ELEMENT_NORMAL_CLOSURE
RADICAL_ELEMENT_PAIR
RADICAL_ELEMENT_POW
RADICAL_ELEMENT_ROOT
RADICAL_ELEMENT_SUB
RADICAL_EQ_INTERS_MINIMAL_PRIMES
RADICAL_EQ_INTERS_PRIME_IDEALS
RADICAL_EXTENSION_BASE
RADICAL_EXTENSION_COMPOSITUM
RADICAL_EXTENSION_CYCLIC_QUOTIENT
RADICAL_EXTENSION_EQ
RADICAL_EXTENSION_EQ_RADICAL_ELEMENTS
RADICAL_EXTENSION_GENERATED_BY_RADICAL_ELEMENTS
RADICAL_EXTENSION_HOMOMORPHIC_IMAGE
RADICAL_EXTENSION_HOMOMORPHIC_IMAGE_GEN
RADICAL_EXTENSION_IMP_FINITE
RADICAL_EXTENSION_INTERMEDIATE
RADICAL_EXTENSION_INTO_SUBFIELD_GENERATED
RADICAL_EXTENSION_ISOMORPHISM
RADICAL_EXTENSION_NORMAL_CLOSURE
RADICAL_EXTENSION_REFL
RADICAL_EXTENSION_ROOT_OF_UNITY
RADICAL_EXTENSION_SIMPLE
RADICAL_EXTENSION_SOLVABLE
RADICAL_EXTENSION_TRANS
RADICAL_EXTENSION_UNIONS
RADICAL_GENERATORS_APPEND
RADICAL_IMP_FIELD_EXTENSION
RADICAL_LOCALIZATION
RADICAL_NORMAL_EXTENSION_SOLVABLE
RADICAL_NUMBER_IMP_RADICAL_ELEMENT
RADICAL_ROOT_SOLVABLE
REAL_CONTINUOUS_ON_QUINTIC
REAL_FRACTION_RING_INTEGER_RING
REAL_RING_PRODUCT
REAL_RING_SUM
REAL_ZPOW_MONO
REAL_ZPOW_MONO_LT
RESIDUE_FIELD_FRACTION
RESIDUE_FIELD_LOCAL_FACTS
RESIDUE_HOM_EQ_0
RESIDUE_HOM_FUNCTORIAL
RESIDUE_HOM_FUNCTORIAL_QUOTIENT
RESTRICTED_PRODUCT_GROUP
RESTRICTED_PRODUCT_GROUP_ALT
RESTRICTED_PRODUCT_GROUP_EQ
RESTRICTED_PRODUCT_GROUP_EQ_PRODUCT_GROUP
RESTRICTED_PRODUCT_GROUP_EQ_SUM_GROUP
RESTRICTED_PRODUCT_GROUP_MONO
RESTRICTED_PRODUCT_GROUP_UNIONS
RESTRICTED_PRODUCT_RING
RESTRICTED_PRODUCT_RING_ALT
RESTRICTED_PRODUCT_RING_EQ
RESTRICTED_PRODUCT_RING_EQ_PRODUCT_RING
RESTRICTED_PRODUCT_RING_MONO
RESTRICTED_PRODUCT_RING_UNIONS
RESTRICTION_IN_RING_HOMOMORPHISM_EXTENSIONS
RESTRICT_PERMUTES_EQ
RIGHT_COSET_AS_IMAGE
RIGHT_COSET_MONO
RIGHT_COSET_PREIMAGE
RIGHT_COSET_SEQUENCES_EQ
RIGHT_COSET_SUBSET_RIGHT_COSET
RING_1_IN_MULTSYS
RING_ADDITIVE_GROUP
RING_ADDITIVE_GROUP_PRODUCT_RING
RING_ADDITIVE_GROUP_RESTRICTED_PRODUCT_RING
RING_ASSOCIATES_X_MINUS_A
RING_AUTOMORPHISM_CNJ
RING_AUTOMORPHISM_COMPOSE
RING_CHARPOLY
RING_CHARPOLY_COEFF_0
RING_CHARPOLY_COEFF_TRACE
RING_CHARPOLY_DEG_COEFF
RING_CHARPOLY_EIGENVECTOR
RING_CHARPOLY_ENTRY
RING_CHARPOLY_EQ
RING_CHARPOLY_EQ_CARD_2
RING_CHARPOLY_EVAL
RING_CHARPOLY_EXTEND
RING_CHARPOLY_HOMOMORPHISM
RING_CHARPOLY_ID
RING_CHARPOLY_MONIC
RING_CHARPOLY_REINDEX
RING_CHARPOLY_SIMILAR
RING_CHARPOLY_TRANSP
RING_CHAR_FIELD_EXTENSION_COMPLEX_RING
RING_CHAR_POLY_RING
RING_CHAR_POWSER_RING
RING_COFACTOR
RING_COFACTOR_EQ
RING_COFACTOR_EQ_GEN
RING_COFACTOR_INSERT
RING_COFACTOR_INSERT_SWAP
RING_COFACTOR_TRANSP
RING_COSET_CHOICE
RING_COSET_MONO
RING_COSET_SETOPS
RING_COSET_SUBSET_RING_COSET
RING_DEPENDENT_EQ
RING_DEPENDENT_MONOMORPHIC_IMAGE
RING_DEPENDENT_ONE
RING_DEPENDENT_SING
RING_DET
RING_DET_ADJUGATE_COLUMNS
RING_DET_ADJUGATE_ROWS
RING_DET_BLOCK_TRIANGULAR
RING_DET_CLOSED
RING_DET_CMUL
RING_DET_COEFF_BASIS
RING_DET_COEFF_EQ_0
RING_DET_COEFF_MONIC_REV
RING_DET_COEFF_RING_SUM
RING_DET_COEFF_X_MINUS
RING_DET_COFACTOR
RING_DET_COFACTOR_EXPANSION
RING_DET_COLUMNS_MUL
RING_DET_DEPENDENT_COLUMNS
RING_DET_DEPENDENT_COLUMNS_MUL
RING_DET_DEPENDENT_COLUMNS_MUL_IDEAL
RING_DET_DEPENDENT_ROWS
RING_DET_DEPENDENT_ROWS_MUL
RING_DET_DIAGONAL
RING_DET_EMPTY
RING_DET_EQ
RING_DET_EQ_0_COLUMNS
RING_DET_EQ_0_ROWS
RING_DET_HOMOMORPHISM
RING_DET_I
RING_DET_IDENTICAL_COLUMNS
RING_DET_IDENTICAL_ROWS
RING_DET_INDEPENDENT_COLUMNS
RING_DET_INDEPENDENT_ROWS
RING_DET_KRONECKER
RING_DET_KRONECKER_MOD_DIV
RING_DET_LAPLACE_INSERT
RING_DET_LOWERTRIANGULAR
RING_DET_LOWERTRIANGULAR_MUL
RING_DET_MINOR_SELECTION
RING_DET_MUL
RING_DET_MULTILINEAR
RING_DET_PERMUTE_COLUMNS
RING_DET_PERMUTE_ROWS
RING_DET_REINDEX
RING_DET_ROWS_MUL
RING_DET_ROW_0
RING_DET_ROW_ADD
RING_DET_ROW_CMUL
RING_DET_ROW_COFACTOR_EXPANSION
RING_DET_ROW_EXPANSION
RING_DET_ROW_OPERATION
RING_DET_ROW_OPERATIONS_SUCC
RING_DET_ROW_SUM
RING_DET_SIMILAR
RING_DET_SING
RING_DET_SUBRING
RING_DET_SWAP_COLUMNS
RING_DET_SWAP_ROWS
RING_DET_SYLVESTER
RING_DET_SYLVESTER_EQ_0
RING_DET_SYLVESTER_ROOTS
RING_DET_SYLVESTER_X_MINUS
RING_DET_TRANSP
RING_DET_TRIANGULAR_ROWS
RING_DET_UPPERTRIANGULAR
RING_DET_VANDERMONDE
RING_DET_WEINSTEIN_ARONSZAJN
RING_DIVIDES_CHAIN
RING_DIVIDES_IRREDUCIBLE_ROOT
RING_DIVIDES_PRODUCT_POW
RING_ENDOMORPHISM_POW_CARD
RING_ENDOMORPHISM_ROOT_OF_UNITY
RING_EPIMORPHISM_PREIMAGE_IDEAL_GENERATED
RING_HOMOMORPHISMS_EQ_FROM_RESIDUE_FIELD
RING_HOMOMORPHISMS_EQ_FROM_RING_SPAN
RING_HOMOMORPHISMS_EQ_FROM_SUBFIELD_GENERATED
RING_HOMOMORPHISMS_INDEPENDENT
RING_HOMOMORPHISMS_INDEPENDENT_SET
RING_HOMOMORPHISM_EXTENSIONS_NONEMPTY
RING_HOMOMORPHISM_EXTENSIONS_ROOT
RING_HOMOMORPHISM_EXTENSIONS_SIMPLE
RING_HOMOMORPHISM_EXTENSIONS_SIMPLE_EQ
RING_HOMOMORPHISM_EXTENSIONS_TOWER
RING_HOMOMORPHISM_EXTENSIONS_TOWER_PRODUCT
RING_HOMOMORPHISM_EXTENSIONS_TOWER_SUM
RING_HOMOMORPHISM_FRACTION_RING_INTEGER_RING
RING_HOMOMORPHISM_FRACTION_RING_INTEGER_RING_EXISTS
RING_HOMOMORPHISM_FROM_SUBFIELD_GENERATED
RING_HOMOMORPHISM_LOCALIZATION_MAP
RING_HOMOMORPHISM_MONOMORPHISM_FACTOR
RING_HOMOMORPHISM_MUL_INV
RING_HOMOMORPHISM_PRODUCT_POW
RING_HOMOMORPHISM_RESIDUE_HOM
RING_HOMOMORPHISM_RESTRICTED_PRODUCT
RING_HOMOMORPHISM_RESTRICTED_PRODUCT_COMPONENTWISE
RING_HOMOMORPHISM_RESTRICTED_PRODUCT_PROJECTION
RING_HOMOMORPHISM_SIGN
RING_HOMOMORPHISM_SUBFIELD_INCLUSION
RING_HOMOMORPHISM_SUBRING_GENERATED_SUBSET
RING_HOMOMORPHISM_SUM_MUL
RING_IDEAL_ADD_IN_EQ
RING_IDEAL_IMP_SUBGROUP
RING_IDEAL_JACOBSON_RADICAL
RING_IDEAL_LOCALIZATION_CONTRACTION_EXTENSION
RING_IDEAL_LOCALIZATION_EXTENSION_CONTRACTION
RING_IDEAL_NILRADICAL
RING_IDEAL_SUB_TRANS
RING_INDEPENDENT_CARD_LE_EXTENSION_DEGREE
RING_INDEPENDENT_EQ
RING_INDEPENDENT_MINIMAL_POLYNOMIAL_POWERS
RING_INDEPENDENT_MONOMORPHIC_IMAGE
RING_INDEPENDENT_ONE
RING_INDEPENDENT_SING
RING_INV_MUL_INV
RING_INV_PRODUCT_RING
RING_INV_RESTRICTED_PRODUCT_RING
RING_INV_SUBRING_GENERATED_GEN
RING_IRREDUCIBLE_VAR_MINUS_A
RING_IRREDUCIBLE_X_MINUS_A
RING_ISOMORPHISMS_POLY_TRANSLATE
RING_ISOMORPHISM_LOCALIZATION_AT_PRIME_LOCALIZATION
RING_ISOMORPHISM_LOCALIZATION_LOCALIZATION
RING_ISOMORPHISM_LOCALIZATION_LOCALIZATION_GEN
RING_ISOMORPHISM_LOCALIZATION_MAP
RING_ISOMORPHISM_LOCALIZATION_RESTRICT
RING_ISOMORPHISM_LOCALIZATION_SATURATION
RING_ISOMORPHISM_ONTO_SUBFIELD_IMAGE
RING_ISOMORPHISM_QUOTIENT_RESIDUE_FIELD
RING_ISOMORPHISM_QUOTIENT_RING_IMAGE
RING_LOCALEQUIV_HOMOMORPHIC_IMAGE
RING_LOCALEQUIV_IN_LOCALIZATION_IDEAL
RING_LOCALIZATION_AT_PRIME_IDEAL_BIJ
RING_LOCALIZATION_AT_PRIME_NONUNITS
RING_LOCALIZATION_CONTRACTION_SUBSET
RING_LOCALIZATION_HOMOMORPHISM_EXISTS
RING_LOCALIZATION_POW
RING_LOCALIZATION_PRIME_IDEAL_BIJ
RING_LOCALIZATION_PRIME_IDEAL_SUBSET
RING_MONOMORPHISM_FROBENIUS_ITERATE
RING_MONOMORPHISM_QUOTIENT_CONTRACTION
RING_MONOMORPHISM_UNITS_IMAGE
RING_MULTSYS_HOMOMORPHIC_IMAGE
RING_MULTSYS_MAXIMAL_COMPLEMENT
RING_MUL_EQ_UNITS_CANCEL
RING_MUL_INV_CANCEL
RING_MUL_IN_MULTSYS
RING_MUL_LCANCEL_EQ
RING_MUL_RCANCEL_EQ
RING_NILPOTENT_QUOTIENT_RING
RING_OF_INT_EQ_0_CHAR_0
RING_OF_INT_EQ_CHAR_0
RING_OF_INT_IN_SUBFIELD_GENERATED
RING_OF_INT_ISUM
RING_ORDER_0
RING_ORDER_DIVIDES_MAXIMAL
RING_ORDER_DIVIDES_MAXIMAL_MULTSYS
RING_ORDER_DIVIDES_MAXIMAL_MULTSYS_GEN
RING_ORDER_DIVIDES_MAXIMAL_UNIT
RING_ORDER_EQ_LEAST
RING_ORDER_LCM_EXISTS
RING_ORDER_LCM_EXISTS_MULTSYS
RING_ORDER_MONOMORPHIC_IMAGE
RING_ORDER_NONZERO
RING_ORDER_NONZERO_MULTSYS
RING_ORDER_SUBFIELD_GENERATED
RING_ORDER_SUBRING_GENERATED
RING_POLYNOMIAL_MUL_MATRIX
RING_POLYNOMIAL_X_MINUS_A
RING_POW_EQ
RING_POW_EQ_GEN
RING_POW_EQ_LT
RING_POW_EQ_LT_EQ
RING_POW_FIXPOINTS_BOUND
RING_PRIME_VAR_MINUS_A
RING_PRIME_X_MINUS_A
RING_PRODUCT_CYCLIC_GROUP
RING_PRODUCT_DELETE
RING_PRODUCT_DIFFERENCES
RING_PRODUCT_DIFFERENCES_SQUARE
RING_PRODUCT_GROUP_TRANSLATION
RING_PRODUCT_IN_PRIME_IDEAL
RING_PRODUCT_IN_RING_IDEAL
RING_PRODUCT_LT_2
RING_PRODUCT_PAIRS_LT
RING_PRODUCT_PERMUTE
RING_PRODUCT_POLY_SUBRING_GENERATED
RING_PRODUCT_POW
RING_PRODUCT_POWSER_SUBRING_GENERATED
RING_PRODUCT_POW_NEG
RING_PRODUCT_UNIONS_PAIRWISE_DISJOINT
RING_PRODUCT_X_MINUS_A
RING_PRODUCT_X_MINUS_A_IN_FIXED_FIELD
RING_PRODUCT_ZERO
RING_SIGN
RING_SIGN_COMPOSE
RING_SIGN_I
RING_SIGN_ID
RING_SIGN_IDEMPOTENT
RING_SIGN_INVERSE
RING_SIGN_SWAP
RING_SIMPLE_ALGEBRAIC_EXTENSION_BASIS
RING_SPAN_EQ
RING_SPAN_EQ_IMAGE
RING_SUM_ALTERNATING_SUBSETS
RING_SUM_CYCLIC_GROUP
RING_SUM_DELTA_MUL
RING_SUM_GROUP_TRANSLATION
RING_SUM_LT_2
RING_SUM_MOD_DIV
RING_SUM_MUL_MOD_DIV
RING_SUM_MUL_SWAP
RING_SUM_NUMSEG_LT_ADD
RING_SUM_PERMUTATIONS_COMPOSE_L
RING_SUM_PERMUTATIONS_COMPOSE_R
RING_SUM_PERMUTATIONS_INVERSE
RING_SUM_PERMUTATIONS_RYSER
RING_SUM_PERMUTE
RING_SUM_POLY_SUBRING_GENERATED
RING_SUM_POWSER_SUBRING_GENERATED
RING_SUM_PRODUCT_CARTESIAN_PRODUCT
RING_SUM_PROD_RING
RING_SUM_SWAP_DELTA
RING_SUM_SYLVESTER_ROWS
RING_SUM_TRACE_SIMILAR
RING_SUM_TRACE_SIMILAR_UNIT
RING_SUM_UNIONS_PAIRWISE_DISJOINT
RING_TRACE_DET_SIMILAR_DIAGONAL
RING_UNIT_LEADING_COEFF_VARPOW_ADD
RING_UNIT_LIFT_JACOBSON_RADICAL
RING_UNIT_MOD_NIL_IDEAL
RING_UNIT_MUL_MATRIX_POLY
RING_UNIT_PRODUCT_RING
RING_UNIT_PROD_RING
RING_UNIT_RESTRICTED_PRODUCT_RING
RING_UNIT_SUBRING_GENERATED
RING_UNIT_SUBRING_OF_FIELD
RING_UNIT_VAR_MINUS_A
RING_UNIT_X_MINUS_A
ROOTS_OF_UNITY_BOUND
ROOTS_OF_UNITY_EQ_MOD_IDEAL
ROOTS_OF_UNITY_HAS_SIZE_DIVISOR
ROOTS_OF_UNITY_HAS_SIZE_IMP_CHAR
ROOTS_OF_UNITY_HAS_SIZE_NONZERO
ROOTS_OF_UNITY_HAS_SIZE_PRIMITIVE
ROOTS_OF_UNITY_RING_ORDER
ROOTS_OF_UNITY_RING_ORDER_DIVISOR
SECOND_COUNTABLE_EUCLIDEAN
SECOND_GROUP_ISOMORPHISM_THEOREM
SECOND_GROUP_ISOMORPHISM_THEOREM_EXPLICIT
SEPARABLE_DEGREE
SEPARABLE_DEGREE_EQ_1
SEPARABLE_DEGREE_EQ_EXTENSION_DEGREE
SEPARABLE_DEGREE_LE_EXTENSION_DEGREE
SEPARABLE_DEGREE_SEPARABLE_CLOSURE
SEPARABLE_DEGREE_SIMPLE
SEPARABLE_DEGREE_SIMPLE_LT
SEPARABLE_DEGREE_TOWER
SEPARABLE_ELEMENT_CHAR0
SEPARABLE_ELEMENT_IMAGE
SEPARABLE_ELEMENT_IMP_ALGEBRAIC
SEPARABLE_ELEMENT_INTERMEDIATE
SEPARABLE_ELEMENT_MONOMORPHIC_IMAGE
SEPARABLE_ELEMENT_POW_EXISTS
SEPARABLE_ELEMENT_POW_IN_IMAGE
SEPARABLE_EXTENSION_BOUNDED_DEGREE
SEPARABLE_EXTENSION_CHAR0
SEPARABLE_EXTENSION_EQ_SEPARABLE_CLOSURE
SEPARABLE_EXTENSION_GENERATED_BY_SEPARABLE
SEPARABLE_EXTENSION_INTERMEDIATE
SEPARABLE_EXTENSION_ISOMORPHISM
SEPARABLE_EXTENSION_REFL
SEPARABLE_EXTENSION_SEPARABLE_CLOSURE
SEPARABLE_EXTENSION_SIMPLE
SEPARABLE_EXTENSION_SUBFIELD
SEPARABLE_EXTENSION_TRANS
SEPARABLE_EXTENSION_TRANS_EQ
SEPARABLE_IMP_ALGEBRAIC_EXTENSION
SEPARABLE_IMP_FIELD_EXTENSION
SHORT_EXACT_SEQUENCE_TRIVIALITY
SIMPLE_ALGEBRAIC_EXTEND_HOMOMORPHISM_ROOT
SOLVABLE_BY_RADICALS_EQ
SOLVABLE_BY_RADICALS_IRREDUCIBLE_EQ
SOLVABLE_GALOIS_RADICAL_ROOT_OF_UNITY
SOLVABLE_GALOIS_RADICAL_TOWER
SOLVABLE_GALOIS_SUBEXTENSION
SOLVABLE_GALOIS_TOWER
SOLVABLE_GROUP_CYCLIC_CHAIN
SOLVABLE_GROUP_CYCLIC_CHAIN_EQ
SOLVABLE_GROUP_NONTRIVIAL_ABELIAN_QUOTIENT
SOLVABLE_GROUP_PRIME_ORDER_CHAIN
SOLVABLE_IMP_RADICAL
SOLVABLE_IMP_RADICAL_EXTENSION
SOLVABLE_IMP_RADICAL_ROOT_OF_UNITY
SOLVABLE_SIMPLE_GROUP
SPLITTING_EQ_FINITE_NORMAL_EXTENSION
SPLITTING_EXTENSION_DEGREE_DIVIDES_FACT
SPLITTING_EXTENSION_EXISTS
SPLITTING_EXTENSION_EXISTS_BIGENOUGH
SPLITTING_EXTENSION_EXISTS_ID
SPLITTING_EXTENSION_EXTEND_HOMOMORPHISM
SPLITTING_EXTENSION_FACTOR
SPLITTING_EXTENSION_GENERATED
SPLITTING_EXTENSION_GENERATED_BY_ROOTS
SPLITTING_EXTENSION_I
SPLITTING_EXTENSION_IMAGE
SPLITTING_EXTENSION_IMAGES_EQ
SPLITTING_EXTENSION_IMP_NORMAL
SPLITTING_EXTENSION_IN_POLY_RING
SPLITTING_EXTENSION_LIFT
SPLITTING_EXTENSION_NONZERO
SPLITTING_EXTENSION_SPLITS
SPLITTING_EXTENSION_UNIQUE
SPLITTING_EXTENSION_UNIQUE_EXPLICIT
SPLITTING_IMP_ALGEBRAIC_EXTENSION
SPLITTING_IMP_FIELD_EXTENSION
SPLITTING_IMP_FINITELY_GENERATED_EXTENSION
SPLITTING_IMP_FINITE_EXTENSION
SUBFIELD_GENERATED_IDEMPOT_GEN
SUBFIELD_GENERATED_INSERT
SUBFIELD_GENERATED_INSERT_FRACTIONS
SUBFIELD_GENERATED_SIMPLE_ALGEBRAIC
SUBFIELD_OF_COMMON_FIXPOINTS
SUBFIELD_OF_FIXED_FIELD
SUBFIELD_OF_RADICAL_ELEMENTS
SUBFIELD_OF_SEPARABLE_CLOSURE
SUBFIELD_OF_UNIONS_DIRECTED
SUBGROUP_GENERATED_GALOIS_GROUP
SUBGROUP_INTER_CARD_DIVIDES
SUBGROUP_MODULAR_EQ
SUBGROUP_OF_GALOIS_GROUP
SUBGROUP_POSITIVE_REALS
SUBGROUP_RESTRICTED_PRODUCT_GROUP
SUBNORMAL_CHAIN_SUBGROUPS
SUBRING_GENERATED_INSERT
SUBRING_IMP_SUBGROUP_ADDITIVE
SUBRING_OF_PRODUCT_RING_EQUALIZER
SUBRING_OF_PROD_RING_EQUALIZER
SUBRING_RESTRICTED_PRODUCT_RING
SUBSET_GALOIS_GROUP_FIXED_FIELD
SUM_GROUP_SUBGROUP_OF_RESTRICTED_PRODUCT_GROUP
SYLOW_SUBGROUP_COUNT_1_NORMAL
THIRD_GROUP_ISOMORPHISM_THEOREM
THIRD_GROUP_ISOMORPHISM_THEOREM_EXPLICIT
TOPSPACE_POINTWISE_PRODUCT
TOPSPACE_POINTWISE_TOPOLOGY
TOPSPACE_QUOTIENT_TOPOLOGY
TRACE_FORM_NONDEGENERATE
TRANSITIVE_TRANSPOSITION_SYMMETRIC_ISOMORPHISM
TRIVIAL_GALOIS_GROUP
UFD_PRIME_POWER_FACTORIZATION
UNIT_GROUP
UNIT_GROUP_POW
UNIT_GROUP_PRODUCT_RING
UNIT_GROUP_PROD_RING
UNIT_GROUP_RESTRICTED_PRODUCT_RING
UNIT_GROUP_SUBRING_GENERATED
UNIT_GROUP_SUM
UPWARD_CLOSED_NUMSEG
UPWARD_CLOSED_NUMSEG_EQ
WEAK_CHAIN_PAIR_BOUND
WEAK_CHAIN_STRICT_STEPS_BOUND
WEAK_CHAIN_STRICT_SUBCHAIN
X_POW_SUB_X_EQ_PRODUCT_IRREDUCIBLES
X_POW_SUB_X_FINITE_FIELD
ZL_SUBSETS_INTERS_NONEMPTY
Removed or changed identifiers:
Files
Library/rabin_test.ml is deleted. Its contents are now in
Library/finite_fields.ml (Rabin's test and three basic facts) and
Library/ringtheory.ml (RING_ENDOMORPHISM_FROBENIUS_ITERATE); load
Library/finite_fields.ml instead.
Theorems removed completely (the auxiliary lemmas of the former
Library/rabin_test.ml, superseded by more general library theorems):
FIELD_NONZERO_PRODUCT_PERMUTE FIELD_ROOTS_BOUND IRREDUCIBLE_DIVIDES_DEGREE
IRREDUCIBLE_DIVIDES_DEGREE_BOUND IRREDUCIBLE_DIVIDES_XQ_MINUS_X
IRREDUCIBLE_DIVIDES_XQ_MINUS_X_GEN POLY_NONUNIT_DEGREE_GE_1
QUOTIENT_POLY_RING_FINITE_CARD RING_DIVIDES_POW_ITERATE RING_DIVIDES_REDUCE
Renamed bindings (the old name now refers only to the like-named core or
other library theorem, which it used to hide when both files were loaded):
REAL_ABS_SIGN (Library/permutations.ml) -> REAL_ABS_SIGN_PERMUTATION
FINITE_INDEX_INRANGE_2 (Multivariate/cvectors.ml) -> FINITE_INDEX_INRANGE_4
DIVISION_0 (Library/transc.ml) -> DIVISION_0_DSIZE
SUM_DIFFS (Library/transc.ml) -> PSUM_DIFFS
NORM_CROSS (Multivariate/flyspeck.ml) -> NORM_CROSS_SIN
PERMUTATION (Permutation/permutation.ml, the definition theorem of the
unchanged constant PERMUTATION) -> PERMUTATION_DEF
LIST_CASES_TAC (4CT/kempe.ml, three-argument tactic) -> X_LIST_CASES_TAC
Constant replaced
minimal_polynomial: the local constant of 100/transcendence.ml
(minimal_polynomial z, for complex z) is replaced by the general constant
minimal_polynomial (k,l) h x of Library/fieldtheory.ml; the old meaning is
minimal_polynomial (QinC_ring,complex_ring) I z
(MINIMAL_POLYNOMIAL_QINC_COMPLEX).
Restated accordingly in 100/transcendence.ml:
algebraic_has_minimal_polynomial maybe_algebraic_minimal_polynomial
minimal_polynomial_QinC complex_root_minimal_polynomial_refl
minimal_polynomial_divides minimal_squarefree_from_algebraic_set
Existing theorems restated with a more general or different statement
RING_MUL_LCANCEL, RING_MUL_RCANCEL: need only a regular element, not a unit
POLY_DEG_CMUL: conditional conclusion instead of hypotheses; also
multivariate
POLY_DEG_MUL_X_MINUS_A: conditional conclusion, no integral domain needed
POLY_DEG_VAR_POW, POLY_DERIV_VAR_POW: stated with poly_pow and poly_mul
POLY_CONST_SUBRING_GENERATED: now quantifies a (before: an unused c, a free)
POLY_IRREDUCIBLE_IMP_SEPARABLE, POLY_NONCONSTANT_IRREDUCIBLE_IMP_SEPARABLE,
POLY_SEPARABLE_IMP_SQUAREFREE, POLY_SQUAREFREE_IMP_SEPARABLE,
POLY_SEPARABLE_EQ_SQUAREFREE: stated with the new constant poly_separable
instead of coprimality with the derivative (the same notion)
FIELD_EXTENSION_INTO_SUBFIELD_GENERATED, RING_SPAN_EMPTY: redundant
hypotheses dropped
FIELD_EXTENSION_FROM_SUBRING_GENERATED: now quantifies s (before free)
ALGEBRAICALLY_CLOSED_FIELD_DECOMPOSE: hypotheses combined into one
antecedent
Existing theorems changed only by renaming bound variables
Library/symmetric_group.ml (sigma, tau): SYMMETRIC_GROUP_POW
SYMMETRIC_GROUP_POW_IN PRIME_ORDER_PERM_NO_FIXPOINT PRIME_ORDER_POW_PERM
PRIME_ORDER_PERM_ORBIT SWAP_CONJUGATE_IN_SUBGROUP
TRANSPOSITION_PCYCLE_GENERATES TRANSITIVE_TRANSPOSITION_GENERATES_SYMMETRIC
Examples/digit_serial_methods.ml (sigma, tau): THEOREM_V_1 COROLLARY_V_3
FULL_COROLLARY BOUND_THEOREM_DIV BOUND_THEOREM_SQRT
Moved from Library/rabin_test.ml to Library/finite_fields.ml (f -> k, and
r -> n in the last): RABIN_IRREDUCIBILITY_NECESSARY
RABIN_IRREDUCIBILITY_SUFFICIENT RABIN_IRREDUCIBILITY_TEST
FINITE_FIELD_POW_ITERATE
Moved with unchanged statements
INDUCT_MATRIX_ROW_OPERATIONS INDUCT_MATRIX_ELEMENTARY
INDUCT_MATRIX_ELEMENTARY_ALT: Multivariate/measure.ml ->
Multivariate/determinants.ml
FINITE_FIELD_ELEMENT_POW FINITE_FIELD_CARD_CHAR_POWER:
Library/rabin_test.ml -> Library/finite_fields.ml
RING_ENDOMORPHISM_FROBENIUS_ITERATE: Library/rabin_test.ml ->
Library/ringtheory.ml
Functions and tactics with changed behaviour
prioritize_complex() (Multivariate/complexes.ml) now calls
prioritize_real() first, so real comes below complex for the other
overloaded symbols
ASSERT_TAC (Permutation/morelist.ml) now finishes with STRIP_ASSUME_TAC,
like the ASSERT_TAC of Multivariate/misc.ml
New OCaml-level functions (not theorems or constants)
RING_HOMOMORPHISM_PUSH_CONV (Library/ringtheory.ml)
X_LIST_CASES_TAC (4CT/kempe.ml, the renamed LIST_CASES_TAC)
Load dependencies
Library/fieldtheory.ml now loads Library/ring_det.ml; Multivariate/canal.ml
now loads Multivariate/measure.ml; 100/transcendence.ml now loads
Library/fieldtheory.ml. Several files now set the number priority they
need explicitly (see the commit message).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.