diff options
| author | Cyril Cohen | 2020-09-24 16:56:04 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-28 10:32:11 +0200 |
| commit | 97ccfcfb1e48d7a203ee61543e882baa3f71895f (patch) | |
| tree | b19cbb0b7b2b510645f845e80994505cf0f2c2b1 /CHANGELOG_UNRELEASED.md | |
| parent | a97b433c2d81c702fe690101a6e4e7afb4a3c28d (diff) | |
Injectivity for additive functions and mulmxr.
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0a59193..b08875c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -137,6 +137,13 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). dual lattices. - in `matrix.v` new lemma `det_mx11`. +- in `ssralg.v`, new lemma `raddf_inj`, characterizing injectivity for + additive maps. +- in `mxalgebra.v`, new lemma `row_free_injr` which duplicates + `row_free_inj` but exposing `mulmxr` for compositionality purposes + (e.g. with `raddf_eq0`), and lemma `inj_row_free` characterizing + `row_free` matrices `A` through `v *m A = 0 -> v = 0` for all `v`. + ### Changed |