diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 0e61ee4fb..1646d76f7 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -2,6 +2,18 @@
 
 ## [Unreleased]
 
+### Renamed
+- in `functions.v`
+  + lemma `scalrfctE` -> `scalerfctE` (deprecating `scalrfctE`)
+
+### Changed
+- in `functions.v`
+  + lemma `fctE` (include `zerofctE` and `onefctE`)
+
+### Added
+- in `functions.v`:
+  + lemmas `zerofctE`, `onefctE`
+
 ### Added
 - in `set_interval.v`:
   + lemmas `setU_itvob1`, `setU_1itvob`
diff --git a/classical/functions.v b/classical/functions.v
index 588489d5c..0b71117c3 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -2740,11 +2740,17 @@ Lemma mulrfctE (T : Type) (K : pzRingType) (f g : T -> K) :
   f * g = (fun x => f x * g x).
 Proof. by []. Qed.
 
-Lemma scalrfctE (T : Type) (K : pzRingType) (L : lmodType K)
+Lemma scalerfctE (T : Type) (K : pzRingType) (L : lmodType K)
     k (f : T -> L) :
   k *: f = (fun x : T => k *: f x).
 Proof. by []. Qed.
 
+Lemma zerofctE (T : Type) (K : nmodType) x : (0 : T -> K) x = 0.
+Proof. by []. Qed.
+
+Lemma onefctE (T : Type) (K : pzRingType) x : (1 : T -> K) x = 1.
+Proof. by []. Qed.
+
 Lemma cstE (T T': Type) (x : T) : cst x = fun _: T' => x.
 Proof. by []. Qed.
 
@@ -2757,10 +2763,14 @@ Lemma compE (T1 T2 T3 : Type) (f : T1 -> T2) (g : T2 -> T3) :
 Proof. by []. Qed.
 
 Definition fctE :=
-  (cstE, compE, opprfctE, addrfctE, mulrfctE, scalrfctE, exprfctE).
+  (cstE, compE, opprfctE, addrfctE, mulrfctE, scalerfctE, exprfctE,
+   zerofctE, onefctE).
 
 End function_space_lemmas.
 
+#[deprecated(since="mathcomp-analysis 1.17.0", use=scalerfctE)]
+Notation scalrfctE := scalerfctE.
+
 Lemma inv_funK T (R : unitRingType) (f : T -> R) : (f\^-1\^-1)%R = f.
 Proof. by apply/funeqP => x; rewrite /inv_fun/= GRing.invrK. Qed.