From 97ccfcfb1e48d7a203ee61543e882baa3f71895f Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 24 Sep 2020 16:56:04 +0200
Subject: Injectivity for additive functions and mulmxr.

---
 CHANGELOG_UNRELEASED.md | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'CHANGELOG_UNRELEASED.md')

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
 
-- 
cgit v1.2.3