aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/algebra
AgeCommit message (Collapse)Author
2018-11-26correct and improve signature and documentation of FieldMixinGeorges Gonthier
Documentation of FieldUnitMixin and FieldMixin corrected to reflect actual arguments, with mulVf and inv0 made explicit arguments for FieldMixin (they were implicit due to the extended signature of Field.mixin_of). Type of FieldMixin changed to a convertible variant to facilitate construction of on-the-fly in-proof construction of fieldType instances, exposing an idomainType instance.
2018-11-21Merge Arguments and Prenex ImplicitsAnton Trunov
See the discussion here: https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
2018-11-15Tweak code related to canonical mixinsAnton Trunov
Remove some unused canonical mixins. Change simplification behavior of concrete comparison functions to allow for better simplification using unfolding and sebsequent folding back e.g. with `rewrite !eqE /= -!eqE`. A bit of cleanup for `Prenex Implicits` declarations. Document some explanations by G. Gonthier.
2018-10-31fixing local MakefileCyril Cohen
should fix #238
2018-10-26moving countalg and closed_field aroundCyril Cohen
- countalg goes to the algebra package - finalg now get the expected inheritance from countalg - closed_field now contains the construction of algebraic closure for countable fields (previously in countalg) - proof of quantifier elimination for closed field rewritten in a monadic style
2018-10-03[opam]: add dev-repo linksAnton Trunov
This commit fixes the following issue: ```shell $ opam pin add coq-mathcomp-ssreflect --dev [ERROR] "dev-repo" field missing in coq-mathcomp-ssreflect metadata, you'll need to specify the pinning location ``` This commit also changes http to https for the homepage links.
2018-09-11Fixes the doc of ratFlorent Hivert
2018-08-06changing companionmx to a more standard oneCyril Cohen
2018-08-03update ChangeLog and docCyril Cohen
2018-08-01Companion matrix of a polynomialCyril Cohen
2018-07-31Rework the whole Makefile architectureCyril Cohen
- Cleanup, refactoring and generalize the makefile architecture - Reuses @strub math-comp/analysis Makefile / Makefile.common organization - As #174, this fixes #88, but looks more stable than trying to fix the use of the MAKEFLAGS internal variable
2018-07-19Merge pull request #202 from CohenCyril/improving-polyLaurent Théry
small generalizations and extensions in poly
2018-07-19poly_size_eq1 phrased with reflect + combinatorsCyril Cohen
2018-07-14updated proposition for big_prod_seq_eq1Cyril Cohen
2018-07-14Laurent's simplificationsCyril Cohen
2018-07-12Replace all the CoInductives with VariantsKazuhiko Sakaguchi
2018-07-04small generalizations in polyCyril Cohen
2018-04-20fix symlinks to README, INSTALL and LICENSEEnrico Tassi
2018-03-04Change deprecated Arguments Scope to ArgumentsJasper Hugunin
2018-02-21Change Implicit Arguments to Arguments in algebraJasper Hugunin
2018-02-06fixing things that @ggonthier and @ybertot spotted and some I spottedCyril Cohen
2018-02-06running semi-automated linting on the whole libraryCyril Cohen
2018-01-26Merge pull request #171 from CohenCyril/mxdirect_deltaCyril Cohen
The spaces generated by some delta_mx are in a direct sum
2017-12-20Merge pull request #172 from CohenCyril/row_mx_eq0Assia Mahboubi
Adding row/col/block_mx_eq0
2017-12-14The spaces generated by some delta_mx are in a direct sumCyril Cohen
proof by @ggonthier
2017-12-14Using x * y = 1 and x / y = 1 to derive the inverseCyril Cohen
fixes #169
2017-12-12Adding row/col/block_mx_eq0Cyril Cohen
2017-11-27following @ggonthier remark.Cyril Cohen
2017-11-23Add addrKA and subrKA (addrK and addrNK modulo Associativity)Cyril Cohen
2017-10-30Fix obsolete vernacular syntax for locality.Maxime Dénès
It was emitting a deprecation warning and will soon be removed from Coq.
2017-10-23Remove compatibility with Coq.8.4 (and compatibility hacks that went with it)Cyril Cohen
2017-10-23Merge pull request #145 from CohenCyril/new-packagerCyril Cohen
New packager
2017-10-19fixed homepageCyril Cohen
2017-10-10fix building with make flagsRalf Jung
Fixes #139
2017-02-04adding rquot_comRingTypeCyril Cohen
2016-11-17Merge remote-tracking branch 'upstream/master' into fixdocFlorent Hivert
2016-11-16Fixes the doc of mxalgebraFlorent Hivert
2016-11-07update copyright bannerAssia Mahboubi
2016-10-24wip shorter proof dec factor theoremsCyril Cohen
2016-08-25Factor theorem for decidable fields, (inspired by PY Strub)Cyril Cohen
2016-08-25Enriched numClosedFieldType so that it factors a lot of theory from both ↵Cyril Cohen
complex and algC. The definitions of 'i, conjC, Re, Im, n.-root, sqrtC and their theory have been moved to the numClosedFieldType structure in ssrnum. This covers boths the uses in algC and complex.v. To that end the numClosedFieldType structure has been enriched with conjugation and 'i. Note that 'i can be deduced from the property of algebraic closure and is only here to let the user chose which definitional equality should hold on 'i. Same thing for conjC that could be written `|x|^+2/x, the only nontrivial (up to my knowledge) property is the fact that conjugation is a ring morphism.
2016-03-15Merge pull request #34 from strub/masterEnrico
all_algebra now exports zmodp
2016-03-15all_algebra now exports zmodpPierre-Yves Strub
2016-02-06typo in int divn1 -> divz1thery
2015-12-12switch ":" to "-"Cyril Cohen
2015-12-04Add finLmodType, finLalgType and finAlgType instancesGeorges Gonthier
2015-12-04Remove more redundant power type structuresGeorges Gonthier
2015-12-04Correct join values to baseFingroupTypeGeorges Gonthier
These were all GRing.Zmodule.sort, instead of the corresponding sort in GRing (Ring.sort, Comin.sort, etc).
2015-12-04Add missing exportGeorges Gonthier
2015-11-10fix INSTALL symlinksEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-03 08:38:28 +0000