Library Algebra.ModuleSpace.ModuleSpace_R_compl
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Complements on module spaces on the ring of real numbers.
Some results need that the ring of scalars is commutative, or being ordered.
Such results are stated here in the case of the ring of real numbers R_Ring.
For generic results that do not need additional assumption on the ring of
scalars, see Algebra.ModuleSpace.ModuleSpace_compl.
These are only stated for the ring of real numbers R_Ring.
Let E1 E2 : ModuleSpace R_Ring.
Let d m be natural numbers.
This module may be used through the import of Algebra.ModuleSpace.ModuleSpace,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
Additional definitions for commutative rings of scalars
- Rn_PreHilbert is the type 'R^n endowed with a PreHilbert structure using dot_product.
- FRd d := 'R^d → R is the type of functions from 'R^d to R.
- FRdm d m := 'R^d → 'R^m is the type of functions from 'R^d to 'R^m.
Usage
From Requisite Require Import stdlib_wR ssr_wMC.
From Coquelicot Require Import Hierarchy.
Close Scope R_scope.
From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Monoid Group Ring.
From Algebra Require Import ModuleSpace_compl ModuleSpace_FF_FT.
From Algebra Require Import ModuleSpace_lin_comb ModuleSpace_lin_map.
From Algebra Require Import ModuleSpace_sub.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Local Open Scope ModuleSpace_scope.
Section ModuleSpace_R_Facts.
Context {E : ModuleSpace R_Ring}.
Lemma scal_comm_R : ∀ a1 a2 : R, scal a1 a2 = scal a2 a1.
Proof. unfold scal; simpl; apply mult_comm_R. Qed.
Lemma scal_sym_R : ∀ a b (u : E), scal a (scal b u) = scal b (scal a u).
Proof. intros; rewrite 2!scal_assoc mult_comm_R; easy. Qed.
Lemma scal_pos_R : ∀ a : R, (0 ≤ scal a a)%R.
Proof. unfold scal; simpl; apply mult_pos_R. Qed.
Lemma scal_zero_rev_R : ∀ (a : R) (u : E), scal a u = 0 → a = 0 ∨ u = 0.
Proof. move=>>; rewrite -non_invertible_equiv_R; apply scal_zero_rev. Qed.
Lemma scal_not_zero_R :
∀ (a : R) (u : E), a ≠ 0 → u ≠ 0 → scal a u ≠ 0.
Proof. move=>>; rewrite -invertible_equiv_R; apply scal_not_zero. Qed.
Lemma scal_def_R : ∀ a : R, scal a a = 0 → a = 0.
Proof. apply Rsqr_0_uniq. Qed.
Lemma scal_reg_l_R :
∀ (a1 a2 : R) (u : E), u ≠ 0 → scal a1 u = scal a2 u → a1 = a2.
Proof.
intros a1 a2 u; rewrite -(minus_zero_equiv a1 a2) -non_invertible_equiv_R.
apply: scal_reg_l.
Qed.
Lemma scal_reg_r_R :
∀ (a : R) (u1 u2 : E), a ≠ 0 → scal a u1 = scal a u2 → u1 = u2.
Proof. move=>>; rewrite -invertible_equiv_R; apply scal_reg_r. Qed.
Lemma scal_zero_reg_l_R :
∀ (a1 : R) (u : E), u ≠ 0 → scal a1 u = 0 → a1 = 0.
Proof. move=>>; rewrite -non_invertible_equiv_R; apply scal_zero_reg_l. Qed.
Lemma scal_zero_reg_r_R :
∀ (a : R) (u1 : E), a ≠ 0 → scal a u1 = 0 → u1 = 0.
Proof. move=>>; rewrite -invertible_equiv_R; apply scal_zero_reg_r. Qed.
Lemma axpy_equiv_R :
∀ (a : R) (u v w : E),
a ≠ 0 → w = scal a u + v ↔ u = scal (/ a)%R w - scal (/ a)%R v.
Proof. move=>> /invertible_equiv_R Ha; rewrite -inv_eq_R axpy_equiv; easy. Qed.
Lemma scalF_nonneg :
∀ {n} (a b : 'R^n),
(∀ i, (0 ≤ a i)%R) → (∀ i, (0 ≤ b i)%R) →
∀ i, (0 ≤ scalF a b i)%R.
Proof. intros; apply Rmult_le_pos; easy. Qed.
End ModuleSpace_R_Facts.
Section ModuleSpace_FF_R_Facts.
Properties on real module spaces.
Properties of operator scalF.
Lemma scalF_scal_r_R :
∀ {n} a x (u : 'E^n), scalF a (scal x u) = scal x (scalF a u).
Proof.
intros; apply extF; intro; rewrite scalF_scal_r fct_scal_r_eq
!scalF_correct constF_correct scal_comm_R scal_assoc; easy.
Qed.
Lemma lm_fct_scalF_r :
∀ {n} (a : 'R^n) (f : '(E → F)^n) i,
lin_map (f i) → lin_map (scalF a f i).
Proof.
move=>> [Hf1 Hf2]; split; move=>>; rewrite !fct_scalF_r_eq !scalF_correct.
rewrite Hf1; apply scal_distr_l.
rewrite Hf2; apply scal_sym_R.
Qed.
End ModuleSpace_FF_R_Facts.
Section Euclidean_space_FF_R_Facts.
Properties of operator scalF.
Lemma scalF_comm_R : ∀ {n} (x y : 'R^n), scalF x y = scalF y x.
Proof. intros; apply extF; intro; apply scal_comm_R. Qed.
Lemma scalF_zero_rev_R :
∀ {n} (a u : 'R^n.+1) i, scalF a u = 0 → a i = 0 ∨ u i = 0.
Proof.
intros n a u i H.
destruct (scal_zero_rev_R _ _ (extF_rev _ _ H i)); [left | right]; easy.
Qed.
Lemma scalF_not_zero_R :
∀ {n} (a u : 'R^n.+1) i, a i ≠ 0 → u i ≠ 0 → scalF a u ≠ 0.
Proof. intros n a u i Ha Hu H; destruct (scalF_zero_rev_R _ _ i H); easy. Qed.
End Euclidean_space_FF_R_Facts.
Section Lin_comb_R_Facts.
Lemma lc_ge_0 : ∀ {n} (L : 'R^n) (B : 'R^n),
(∀ i, (0 ≤ L i)%R) → (∀ i, (0 ≤ B i)%R) → (0 ≤ lin_comb L B)%R.
Proof. intros; apply sum_nonneg_R, scalF_nonneg; easy. Qed.
Lemma lc_comm_R :
∀ {n} (L1 L2 : 'R^n), lin_comb L1 L2 = lin_comb L2 L1.
Proof. intros; apply lc_scalF_compat, scalF_comm_R. Qed.
Context {E : ModuleSpace R_Ring}.
Lemma lc_scal_r :
∀ {n} x L (B : 'E^n), lin_comb L (scal x B) = scal x (lin_comb L B).
Proof.
intros; unfold lin_comb; rewrite scalF_scal_r_R scal_sum_distr_l; easy.
Qed.
Lemma lc_lm_r : ∀ {n} L, lin_map (lin_comb L : 'E^n → E).
Proof. intros n L; split; move=>>; [apply lc_plus_r | apply lc_scal_r]. Qed.
Lemma lc2_l_alt_sym :
∀ {n1 n2} {L1} {B1 : 'E^n1} {L12} {B2 : 'E^n2},
(∀ i1, B1 i1 = lin_comb (L12 i1) B2) →
lin_comb L1 B1 = lin_comb (mapF (lin_comb^~ L1) (flipT L12)) B2.
Proof.
move=>> H; rewrite (lc2_l_alt H); f_equal; apply extF; intro; apply lc_comm_R.
Qed.
Lemma lc2_r_sym :
∀ {n1 n2} L1 L2 (B12 : 'E^{n1,n2}),
lin_comb L2 (lin_comb L1 B12) = lin_comb L1 (lin_comb L2 (flipT B12)).
Proof. intros; rewrite lc_flipT_r f_lc_compat_lm; [easy | apply lc_lm_r]. Qed.
Lemma lc_invalF_aux1 :
∀ {n1 n2} L1 (B1 : 'E^n1) (B2 : 'E^n2), invalF B1 B2 →
injective B2 →
let L2 := (fun i2 ⇒ lin_comb (charac (fun i1 ⇒ B1 i1 = B2 i2)) L1) in
lin_comb L1 B1 = lin_comb L2 B2.
Proof.
intros n1 n2 L1 B1 B2 HB H2 L2.
induction n1.
rewrite lc_nil.
apply eq_sym, lc_zero_compat_l, extF; intro.
rewrite zeroF; unfold L2; rewrite lc_zero_compat_l; try easy.
apply extF; intros [i1 Hi1].
contradict Hi1; auto with arith.
unfold L2; rewrite lc_ind_l.
rewrite IHn1; try now apply liftF_S_invalF.
destruct (invalF_fun HB) as [f Hf].
rewrite (Hf ord0).
rewrite -lc_plus_kron_l.
apply lc_eq_l, extF; intros i2.
rewrite fct_plus_eq fct_scal_r_eq.
destruct (ord_eq_dec (f ord0) i2) as [Hi2 | Hi2].
rewrite kron_is_1; try now f_equal.
rewrite scal_one_r; try easy.
rewrite lc_ind_l.
rewrite liftF_S_charac.
f_equal.
rewrite charac_is_1.
now rewrite scal_one.
rewrite -Hi2; easy.
rewrite kron_is_0; try now (contradict Hi2; apply ord_inj).
rewrite scal_zero_r plus_zero_l.
rewrite lc_ind_l.
rewrite → scal_zero_compat_l, plus_zero_l.
apply lc_eq_l, extF; intros i1.
case (charac_or (fun i0 : 'I_n1 ⇒ B1 (lift_S i0) = B2 i2) i1); intros H.
rewrite H; apply charac_out_equiv in H.
apply eq_sym, charac_is_0; easy.
rewrite H; apply (charac_in_equiv _ i1) in H.
apply eq_sym, charac_is_1; easy.
apply charac_is_0.
intros HK.
apply Hi2; f_equal; apply H2.
rewrite <- Hf; easy.
Qed.
Lemma lc_invalF_aux2 :
∀ {n1 n2} L1 (B1 : 'E^n1) (B2 : 'E^n2),
invalF B1 B2 →
(∀ i j, B2 i = B2 j → B2 i ≠ 0 → i = j) →
let L2 := fun i2 ⇒
scal (charac (fun i ⇒ B2 i ≠ 0) i2)
(lin_comb (charac (fun i1 ⇒ B1 i1 = B2 i2)) L1) in
lin_comb L1 B1 = lin_comb L2 B2 ∧ ∀ i, B2 i = 0 → L2 i = 0.
Proof.
intros n1 n2 L1 B1 B2 HB H2 L2.
induction n1.
rewrite lc_nil; split.
apply eq_sym, lc_zero_compat_l, extF; intros i2.
unfold L2; rewrite lc_zero_compat_l.
rewrite scal_zero_r; easy.
apply extF; intros i1.
destruct i1 as (n,Hn).
contradict Hn; auto with arith.
intros i2 Hi2; unfold L2.
rewrite lc_zero_compat_l.
rewrite scal_zero_r; easy.
apply extF; intros i1.
destruct i1 as (n,Hn).
contradict Hn; auto with arith.
split; unfold L2.
rewrite lc_ind_l.
destruct (IHn1 (fun i : 'I_n1 ⇒ L1 (lift_S i))
(fun i : 'I_n1 ⇒ B1 (lift_S i)) ) as (T1,T2); try easy.
rewrite T1; clear T1 T2.
destruct (invalF_fun HB) as [f Hf].
rewrite (Hf ord0).
rewrite -lc_plus_kron_l.
apply lc_scalF_compat, extF; intros i2; rewrite 2!scalF_correct.
case (charac_or (fun i : 'I_n2 ⇒ B2 i ≠ 0) i2); intros HZ; rewrite HZ.
replace (B2 i2) with (@zero E).
rewrite 2!scal_zero_r; easy.
apply charac_out_equiv in HZ.
unfold Subset.compl in HZ.
case (classic (B2 i2 = 0)); try easy.
apply (charac_in_equiv _ i2) in HZ; simpl in HZ.
f_equal.
rewrite scal_one fct_plus_eq fct_scal_r_eq.
case (ord_eq_dec (f ord0) i2); intros Hi2.
rewrite kron_is_1; try now f_equal.
rewrite scal_one_r; try easy.
rewrite charac_is_1; try easy.
rewrite scal_one.
rewrite lc_ind_l.
rewrite liftF_S_charac.
f_equal.
rewrite charac_is_1.
now rewrite scal_one.
rewrite -Hi2; apply Hf.
rewrite kron_is_0; try now (contradict Hi2; apply ord_inj).
rewrite scal_zero_r plus_zero_l.
rewrite charac_is_1; try easy.
rewrite scal_one.
rewrite lc_ind_l.
rewrite liftF_S_charac.
rewrite charac_is_0.
rewrite scal_zero_l plus_zero_l; easy.
intros HK.
apply Hi2; symmetry; f_equal; apply H2; try easy.
rewrite <- Hf; easy.
intros i2 Hi2.
rewrite charac_is_0; try easy.
rewrite scal_zero_l; easy.
Qed.
Lemma lc_invalF :
∀ {n1 n2} L1 (B1 : 'E^n1) (B2 : 'E^n2),
invalF B1 B2 →
∃ L2, lin_comb L1 B1 = lin_comb L2 B2 ∧
let C2 := fun i2 ⇒
scal (charac (fun j2 : 'I_n2 ⇒
∀ k2 : 'I_n2, (k2 < j2)%coq_nat → B2 j2 ≠ B2 k2) i2) (B2 i2) in
L2 = fun i2 ⇒
scal (charac (fun j2 ⇒ C2 j2 ≠ 0) i2)
(lin_comb (charac (fun i1 ⇒ B1 i1 = C2 i2)) L1).
Proof.
intros n1 n2 L1 B1 B2 HB.
pose (B3 := fun i2:'I_n2 ⇒ scal
(charac (fun z:'I_n2 ⇒ ∀ j2:'I_n2, (j2 < z)%coq_nat → B2 z ≠ B2 j2) i2)
(B2 i2)); fold B3.
assert (H1: ∀ i:'I_n2, B3 i = B2 i ∨ B3 i = 0).
intros i2.
unfold B3; case (charac_or
(fun z : 'I_n2 ⇒ ∀ j2 : 'I_n2,
(j2 < z)%coq_nat → B2 z ≠ B2 j2) i2); intros HZ; rewrite HZ.
right; rewrite scal_zero_l; easy.
left; apply: scal_one.
generalize (lc_invalF_aux2 L1 B1 B3).
pose (L3:= fun i2 : 'I_n2 ⇒
scal
(charac (fun i : 'I_n2 ⇒ B3 i ≠ 0) i2)
(lin_comb
(charac
(fun i1 : 'I_n1 ⇒ B1 i1 = B3 i2)) L1)); fold L3.
intros T; destruct T as (H3,H4).
intros i1.
destruct (HB i1) as (i2,Hi2).
destruct (arg_min_ex B2 i2) as (i3,(V1,(V2,V3))).
∃ i3.
rewrite Hi2; rewrite <- V2.
unfold B3; rewrite charac_is_1; try easy.
rewrite scal_one; easy.
intros k Hk.
rewrite V2; apply V3; easy.
intros i j H2 H3.
case (charac_or
(fun z : 'I_n2 ⇒ ∀ j2 : 'I_n2,
(j2 < z)%coq_nat → B2 z ≠ B2 j2) i); intros HZi.
contradict H3.
unfold B3; rewrite HZi.
rewrite scal_zero_l; easy.
specialize (proj1 (charac_in_equiv _ i) HZi); simpl; intros HZi2.
case (charac_or
(fun z : 'I_n2 ⇒ ∀ j2 : 'I_n2,
(j2 < z)%coq_nat → B2 z ≠ B2 j2) j); intros HZj.
contradict H3.
rewrite H2; unfold B3; rewrite HZj.
rewrite scal_zero_l; easy.
specialize (proj1 (charac_in_equiv _ j) HZj); simpl; intros HZj2.
case (le_lt_dec i j); intros H4.
case (proj1 (Nat.lt_eq_cases i j) H4); try easy.
intros H5; contradict H2.
unfold B3; rewrite HZi HZj.
rewrite 2!scal_one.
apply sym_not_eq; apply HZj2; easy.
intros H5; apply ord_inj; easy.
contradict H2.
unfold B3; rewrite HZi HZj.
rewrite 2!scal_one.
apply HZi2; easy.
∃ L3; split; try easy.
rewrite H3.
apply lc_scalF_compat.
apply extF; intros i2; rewrite 2!scalF_correct;
case (H1 i2); intros H5; rewrite H5; try easy.
rewrite H4; try easy.
rewrite 2!scal_zero_l; easy.
Qed.
Lemma lc_invalF_injF :
∀ {n1 n2} L1 (B1 : 'E^n1) (B2 : 'E^n2),
injective B1 → injective B2 → invalF B1 B2 →
∃ L2, lin_comb L1 B1 = lin_comb L2 B2 ∧ invalF L1 L2 ∧
(∀ i2, L2 i2 = 0 ∨ inF (L2 i2) L1).
Proof.
intros n1 n2 L1 B1 B2 HB1 HB2 HB.
specialize (lc_invalF_aux1 L1 B1 B2 HB HB2); intros H.
pose (L2:=(fun i2 : 'I_n2 ⇒ lin_comb
(charac (fun i1 : 'I_n1 ⇒ B1 i1 = B2 i2)) L1)); fold L2 in H.
∃ L2.
split; try easy.
split.
intros i1.
destruct (HB i1) as (i2, Hi2).
∃ i2; unfold L2.
destruct n1; try now destruct i1.
rewrite (lc_one_l i1).
rewrite charac_is_1; try easy.
rewrite scal_one; easy.
apply skipF_zero_compat.
intros j1 Hj1.
apply charac_is_0.
intros K; apply Hj1; f_equal.
apply HB1; rewrite K; easy.
intros i2; unfold L2.
case (classic (inF (B2 i2) B1)); intros H1.
destruct H1 as (i1,Hi1).
right; ∃ i1.
destruct n1; try now destruct i1.
rewrite (lc_one_l i1).
rewrite charac_is_1; try easy.
rewrite scal_one; easy.
apply skipF_zero_compat.
intros j1 Hj1.
apply charac_is_0.
intros K; apply Hj1; f_equal.
apply HB1; rewrite K; easy.
left.
apply (lc_zero_compat_l _ L1), extF; intros i1.
apply charac_is_0.
intros K; apply H1.
∃ i1; easy.
Qed.
End Lin_comb_R_Facts.
Section Dot_product_R_Facts.
Lemma dot_product_scal_r :
∀ {n} (u v : 'R^n) a, u ⋅ scal a v = a × (u ⋅ v).
Proof. intros; unfold dot_product; rewrite lc_scal_r; easy. Qed.
Lemma dot_product_plus_r :
∀ {n} (u v w : 'R^n), u ⋅ (v + w) = u ⋅ v + u ⋅ w.
Proof. intros; unfold dot_product; rewrite lc_plus_r; easy. Qed.
Lemma dot_product_ind_r :
∀ {n} (u v : 'R^n.+1),
u ⋅ v = widenF_S u ⋅ widenF_S v + scal (u ord_max) (v ord_max).
Proof. intros; unfold dot_product; rewrite lc_ind_r; easy. Qed.
Lemma dot_product_comm : ∀ {n} (u v : 'R^n), u ⋅ v = v ⋅ u.
Proof. intros; apply lc_comm_R. Qed.
Lemma dot_product_pos : ∀ {n} (u : 'R^n), (0 ≤ u ⋅ u)%R.
Proof.
intros n u; induction n as [| n Hn]; unfold dot_product.
rewrite lc_nil; apply Rle_refl.
rewrite lc_ind_l; apply Rplus_le_le_0_compat; try apply Hn.
apply scal_pos_R.
Qed.
Lemma dot_product_def : ∀ {n} (u : 'R^n), u ⋅ u = 0 → u = 0.
Proof.
intros n u; induction n as [| n Hn].
intros; apply nil_is_zero.
rewrite (dot_product_skipF _ _ ord0); intros Hu.
apply Rplus_eq_R0 in Hu; try apply scal_pos_R; try apply dot_product_pos.
destruct Hu as [Hu0 Hu].
apply (extF_zero_skipF _ ord0); [apply scal_def_R | apply Hn]; easy.
Qed.
End Dot_product_R_Facts.
Section Lin_map_R_Facts.
Context {E F : ModuleSpace R_Ring}.
Lemma lm_fct_scal :
∀ (f : E → F) (l : R), lin_map f → lin_map (scal l f).
Proof.
move=>> [Hf1 Hf2]; split; move=>>; rewrite !fct_scal_r_eq.
rewrite Hf1; apply scal_distr_l.
rewrite Hf2; apply scal_sym_R.
Qed.
Definition lm_fct_scal_r := lm_fct_scal.
End Lin_map_R_Facts.
Section Lin_map_Lin_comb_R_Facts.
Context {E F : ModuleSpace R_Ring}.
Lemma fct_lc_r_lm :
∀ {n} L (f : '(E → F)^n),
(∀ i, lin_map (f i)) → lin_map (lin_comb L f).
Proof.
intros n; induction n as [| n Hn]; move=>> Hf.
rewrite lc_nil; apply lm_fct_zero.
rewrite lc_ind_l; apply lm_fct_plus;
[apply lm_fct_scal; easy | apply Hn; intro; apply Hf].
Qed.
Lemma fct_lc_r_lm_alt :
∀ {n} L (f : '(E → F)^n),
(∀ i, lin_map (f i)) → lin_map (fun x ⇒ lin_comb L (f^~ x)).
Proof.
move⇒ n L f Hf; eapply lm_ext;
[apply fct_lc_r_eq | apply (fct_lc_r_lm L _ Hf)].
Qed.
Lemma f_lc_compat_lms :
∀ {n1 n2} L1 (f1 : '(E → F)^n1) L2 (B2 : 'E^n2),
(∀ i, lin_map (f1 i)) →
lin_comb L1 f1 (lin_comb L2 B2) = lin_comb L2 (mapF (lin_comb L1 f1) B2).
Proof. intros; apply f_lc_compat_lm, fct_lc_r_lm; easy. Qed.
Lemma lm_component_sum : ∀ {n}, lin_map (fun B : 'E^n ⇒ sum B).
Proof. intros; eapply lm_ext; [apply lc_ones_l | apply lc_lm_r]. Qed.
Lemma lm_decomp :
∀ {n1 n2} (f : 'R^n1 → 'R^n2) i2,
lin_map f → f^~ i2 = lin_comb (fun i1 ⇒ f (itemF n1 1 i1) i2).
Proof.
move=>> Hf; apply fun_ext; intros x1.
rewrite -{1}(lc_kron_r x1) f_lc_compat_lm// lc_comm_R fct_lc_r_eq.
apply lc_ext_r; intro; rewrite mapF_correct itemF_kron_eq; f_equal.
apply extF; intro; rewrite mult_one_l; easy.
Qed.
Lemma lm_decomp_1 :
∀ {n} (f : 'R^n → R),
lin_map f → f = lin_comb (fun i ⇒ f (itemF n 1 i)).
Proof.
intros n f Hf; apply (comp_inj_r (constF_inj 0)).
apply fun_ext; intros x; apply extF; intros i.
apply (@fun_ext_rev _ _ ((constF 1 \o f)^~ i)); rewrite lm_decomp//.
apply lm_comp; [easy | apply lm_constF].
Qed.
End Lin_map_Lin_comb_R_Facts.
Section Compatible_ModuleSpace_Lin_map_R_Facts1.
Variable E1 E2 : ModuleSpace R_Ring.
Lemma cms_lm : compatible_ms (@lin_map _ E1 E2).
Proof. split; [apply cg_lm |]; move=>>; apply lm_fct_scal. Qed.
Definition Lm := sub_ModuleSpace cms_lm.
End Compatible_ModuleSpace_Lin_map_R_Facts1.
Section Compatible_ModuleSpace_Lin_map_R_Facts2.
Variable E : ModuleSpace R_Ring.
Definition Endom : (E → E) → Prop := fun f ⇒ lin_map f.
Definition Autom : (E → E) → Prop :=
fun f ⇒ lin_map f ∧ bijective f.
End Compatible_ModuleSpace_Lin_map_R_Facts2.
Section FRd_Def.
Definition FRd d := 'R^d → R.
Definition FRdm d m := 'R^d → 'R^m.
End FRd_Def.