From df5b4c0bd10c92ac9dc067b32e3c43fca45b6b27 Mon Sep 17 00:00:00 2001
From: Takafumi Saikawa <tscompor@gmail.com>
Date: Thu, 4 Jun 2026 01:05:26 +0900
Subject: [PATCH 1/2] add zerofctE and onefctE; rename scalrfctE to scalerfctE

---
 CHANGELOG_UNRELEASED.md | 12 ++++++++++++
 classical/functions.v   | 14 ++++++++++++--
 2 files changed, 24 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 0e61ee4fbc..1646d76f7e 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 588489d5c7..8f1143bb88 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) : (0 : T -> K) = (fun=> 0).
+Proof. by []. Qed.
+
+Lemma onefctE (T : Type) (K : pzRingType) : (1 : T -> K) = (fun=> 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.
 

From 6e5c5728b7614e8c45e6aad6dd3e9c8b9cab023d Mon Sep 17 00:00:00 2001
From: Takafumi Saikawa <tscompor@gmail.com>
Date: Thu, 4 Jun 2026 10:14:29 +0900
Subject: [PATCH 2/2] make onefctE and zerofctE pointwise

---
 classical/functions.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/classical/functions.v b/classical/functions.v
index 8f1143bb88..0b71117c3a 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -2745,10 +2745,10 @@ Lemma scalerfctE (T : Type) (K : pzRingType) (L : lmodType K)
   k *: f = (fun x : T => k *: f x).
 Proof. by []. Qed.
 
-Lemma zerofctE (T : Type) (K : nmodType) : (0 : T -> K) = (fun=> 0).
+Lemma zerofctE (T : Type) (K : nmodType) x : (0 : T -> K) x = 0.
 Proof. by []. Qed.
 
-Lemma onefctE (T : Type) (K : pzRingType) : (1 : T -> K) = (fun=> 1).
+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.