aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/algebra
AgeCommit message (Expand)Author
2020-09-28Update `map_mx_id`, fix some implicits and argument ordersCyril Cohen
2020-09-28Merge pull request #597 from CohenCyril/inj_row_freeaffeldt-aist
2020-09-28Apply suggestions from code reviewKazuhiko Sakaguchi
2020-09-28Redefine itv_bound with BRight_if and BRInfty_ifKazuhiko Sakaguchi
2020-09-28The new interval libraryKazuhiko Sakaguchi
2020-09-28Merge pull request #484 from CohenCyril/ord1Kazuhiko Sakaguchi
2020-09-28Injectivity for additive functions and mulmxr.Cyril Cohen
2020-09-27Putting ord1 in fintypeCyril Cohen
2020-09-24Adding `det_mx11`Cyril Cohen
2020-09-08Adding sub_sums_genmxP (generalizes sub_sumsmxP)Cyril Cohen
2020-09-08Merge pull request #573 from CohenCyril/horner_diagLaurent Théry
2020-09-08Lemma mul_rvPCyril Cohen
2020-09-07Adding [row|col]_[udlr]submx lemmasCyril Cohen
2020-09-07compat Coq < 8.10Cyril Cohen
2020-09-07Refactoring proof of det_trig and spawning sublemmasCyril Cohen
2020-09-07Polynomial evaluation and minimal poly of a diagonal matrixCyril Cohen
2020-09-04Adding more map_mx lemmasCyril Cohen
2020-09-04Merge pull request #575 from CohenCyril/mxOverLaurent Théry
2020-09-03Lemmas reindex_omap and bigD1_ordCyril Cohen
2020-09-03Merge branch 'missing_mxalgebra' of https://github.com/CohenCyril/math-comp i...thery
2020-09-03Lemmas mxminpoly_minP and dvd_mxminpolyCyril Cohen
2020-09-03Adding missing mxalgebra lemmasCyril Cohen
2020-09-03Merge pull request #565 from CohenCyril/split_ordPLaurent Théry
2020-09-03Merge pull request #564 from CohenCyril/pinvmxLaurent Théry
2020-09-03Merge pull request #560 from CohenCyril/commr_hornerLaurent Théry
2020-09-03More pinvmx theoryCyril Cohen
2020-09-03Adding mxOver predicateCyril Cohen
2020-09-03Adding commr_horner lemmaCyril Cohen
2020-09-03Expliciting relation between split and [lr]shiftCyril Cohen
2020-09-03Extracting a nonzero coefficient from a nonzero matrixCyril Cohen
2020-09-03Elementary theory of diagonal and triagular matricesCyril Cohen
2020-08-13Be robust to a change in the default argument naming algorithm.Jasper Hugunin
2020-08-12Get rid of displays in class fields and mixin parametersKazuhiko Sakaguchi
2020-06-24missing lemmas discovered while developing mathcomp-analysisReynald Affeldt
2020-06-09fix coq 8.12 warningsCyril Cohen
2020-06-08silencing warnings in individual packagesCyril Cohen
2020-06-06ImprovementsCyril Cohen
2020-06-06tentative changelogReynald Affeldt
2020-06-06General theory of min and max, and use in ssrnumCyril Cohen
2020-06-05fix namingReynald Affeldt
2020-06-04fix namingReynald Affeldt
2020-06-03add real_* variantsReynald Affeldt
2020-06-02another lemma about norm from mathcomp-analysisReynald Affeldt
2020-05-22tentative change of naming convention and add variantsReynald Affeldt
2020-05-21three lemmas that we found useful in the context of theReynald Affeldt
2020-04-09Merge pull request #473 from affeldt-aist/long_short_suffixesaffeldt-aist
2020-04-09Merge pull request #431 from ppedrot/rm-constr-hint-declsaffeldt-aist
2020-04-09- switching long suffixes to short suffixesReynald Affeldt
2020-04-09Merge pull request #474 from llelf/doc-typosaffeldt-aist
2020-04-08fix typos in documentation: formulaeAntonio Nikishaev
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:53:08 +0000