# Library mathcomp.algebra.sesquilinear

From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
From mathcomp Require Import choice fintype tuple bigop ssralg finset fingroup.
From mathcomp Require Import zmodp poly order ssrnum matrix mxalgebra vector.
Sesquilinear forms u ``_ i := u 0 i e_ j := the row matrix with a 1 in column j M ^ phi := map_mx phi M Notation in scope form_scope. M ^t phi := (M ^T) ^ phi Notation in scope form_scope. involutive_rmorphism R == the type of involutive functions R has type ringType. The HB class is InvolutiveRMorphism. {bilinear U -> U' -> V | s & s'} == the type of bilinear forms which are essentially functions of type U -> U' -> V U and U' are lmodType's, V is a zmodType, s and s' are scaling operations of type R -> V -> V. The HB class is Bilinear. The factory bilinear_isBilinear provides a way to instantiate a bilinear form from two GRing.linear_for proofs. {bilinear U -> V -> W | s } := {bilinear U -> V -> W | s.1 & s.2} {bilinear U -> V -> W} := {bilinear U -> V -> W | *:%R & *:%R } {biscalar U} := {bilinear U -> U -> _ | *%R & *%R } applyr f x := f ^~ x with f : U -> U' -> V form theta M u v == form defined from a matrix M := (u *m M *m (v ^t theta)) 0 0 u and v are row vectors, M is a square matrix, coefficients have type R : fieldType, theta is a morphism {hermitian U for eps & theta} == hermitian/skew-hermitian form eps is a boolean flag, (false -> hermitian, true -> skew-hermitian), theta is a function R -> R (R : ringType). The HB class is Hermitian. *%R is used as a the first scaling operator. theta \; *R is used as the second scaling operation of the bilinear form. The archetypal case is theta being the complex conjugate. M \is (eps, theta).-sesqui == M is a sesquilinear form orthomx theta M B == M-orthogonal completement of B := kermx (M *m B ^t theta) M is a square matrix representing a sesquilinear form, B is a rectangle matrix representing a subspace (local notation: B ^_|_) ortho theta M B == orthomx theta M B with theta a morphism A '_|_ B := (A%MS <= B^_|_)%MS This is a local notation. rad theta M := ortho theta M 1%:M (local notation: 1%:M^_|_) {symmetric U} == symmetric form := {hermitian U for false & idfun} {skew_symmetric U} == skew-symmetric form := {hermitian U for true & idfun} {hermitian_sym U for theta} := hermitian form using theta (eps = false) {dot U for theta} == type of positive definite forms The HB class is Dot. is_skew eps theta form := eps = true /\ theta = idfun is_sym eps theta form := eps = false /\ theta = idfun is_hermsym eps theta form := eps = false ortho_rec s1 s2 := elements of s1 and s2 are pairwise orthogonal pairwise_orthogonal s == elements of s are pairwise orthogonal and s does not contain 0 orthogonal s1 s2 == the inner product of an element of S1 and an element of S2 is 0 := ortho_rec s1 s2 orthonormal s == s is an orthonormal set of unit vectors isometry form1 form2 tau == tau is an isometry from form1 to form2 form1 and form2 are hermitian forms. {in D, isometry tau, to R} == local notation for now orthov (V : {vspace vT}) == the space orthogonal to V In the following definitions, we have f : {hermitian vT for eps & theta} with vT : vectType F (F : fieldType): nondegenerate f == f is non-degenerated is_symplectic f == f is a symplectic bilinear form is_orthogonal f == f is an orthogonal form is_unitary f == f is a unitary form form_of_matrix theta M U V := \tr (U *m M *m (V ^t theta)) matrix_of_form f := \matrix_(i, j) form 'e_i 'e_j M \is hermitianmx eps theta == same as M \is (eps, theta).-sesqui without the constraint that theta is a morphism symmetricmx := hermitianmx _ false idfun skewmx := hermitianmx _ true idfun hermsymmx := hermitianmx _ false conjC
Set Implicit Arguments.
Reserved Notation "u '``_' i"
(at level 3, i at level 2, left associativity, format "u '``_' i").
Reserved Notation "M ^t phi"
(at level 39, left associativity, format "M ^t phi").
Reserved Notation "A ^!" (at level 2, format "A ^!").
Reserved Notation "A ^_|_" (at level 8, format "A ^_|_").
Reserved Notation "A ''_|_' B" (at level 69, format "A ''_|_' B").
Reserved Notation "eps_theta .-sesqui"
(at level 2, format "eps_theta .-sesqui").
Local Open Scope ring_scope.
Import GRing.Theory Order.Theory Num.Theory.
Notation "u '``_' i" := (u 0%R i) : ring_scope.
Notation "''e_' j" := (delta_mx 0 j)
(format "''e_' j", at level 8, j at level 2) : ring_scope.
Notation "M ^ phi" := (map_mx phi M) : form_scope.
Notation "M ^t phi" := ((M ^T) ^ phi) : form_scope.
TODO: move?
Lemma eq_map_mx_id (R : ringType) m n (M : 'M[R]_(m, n)) (f : R → R) :
f =1 id → M ^ f = M.
TODO: move?
#[short(type="involutive_rmorphism")]
HB.structure Definition InvolutiveRMorphism (R : ringType) :=
{ f of @GRing.RMorphism R R f & @isInvolutive R f }.
Section InvolutiveTheory.
Variable R : ringType.
Let idfunK : involutive (@idfun R).
Lemma rmorphK (f : involutive_rmorphism R) : involutive f.
End InvolutiveTheory.
Definition conjC {C : numClosedFieldType} (c : C) : C := c^*.
Section conjC_involutive.
Variable C : numClosedFieldType.
Let conjCfun_involutive : involutive (@conjC C).
End conjC_involutive.
Lemma map_mxCK {C : numClosedFieldType} m n (A : 'M[C]_(m, n)) :
(A ^ conjC) ^ conjC = A.
Structure revop X Y Z (f : Y -> X -> Z) := RevOp { fun_of_revop :> X -> Y -> Z; _ : forall x, f x =1 fun_of_revop^~ x }. Notation " [ 'revop' revop 'of' op ]" := (@RevOp _ _ _ revop op (fun _ _ => erefl)) (at level 0, format " [ 'revop' revop 'of' op ]") : form_scope.
#[short(type="bilinear")]
HB.structure Definition Bilinear (R : ringType) (U U' : lmodType R)
(V : zmodType) (s : R → V → V) (s' : R → V → V) :=
{f of isBilinear R U U' V s s' f}.
Definition bilinear_for (R : ringType) (U U' : lmodType R) (V : zmodType)
(s : GRing.Scale.law R V) (s' : GRing.Scale.law R V) (f : U → U' → V) :=
((∀ u', GRing.linear_for (s : R → V → V) (f ^~ u'))
× (∀ u, GRing.linear_for s' (f u)))%type.
Module BilinearExports.
Module Bilinear.
Section bilinear.
Variables (R : ringType) (U U' : lmodType R) (V : zmodType) (s s' : R → V → V).
Local Notation bilinear f := (bilinear_for *:%R *:%R f).
Local Notation biscalar f := (bilinear_for *%R *%R f).
Support for right-to-left rewriting with the generic linearZ rule.
Notation mapUUV := (@Bilinear.type R U U' V s s').
Definition map_class := mapUUV.
Definition map_at_left (a : R) := mapUUV.
Definition map_at_right (b : R) := mapUUV.
Definition map_at_both (a b : R) := mapUUV.
Structure map_for_left a s_a :=
MapForLeft {map_for_left_map : mapUUV; _ : s a = s_a }.
Structure map_for_right b s'_b :=
MapForRight {map_for_right_map : mapUUV; _ : s' b = s'_b }.
Structure map_for_both a b s_a s'_b :=
MapForBoth {map_for_both_map : mapUUV; _ : s a = s_a ; _ : s' b = s'_b }.
Definition unify_map_at_left a (f : map_at_left a) :=
MapForLeft f (erefl (s a)).
Definition unify_map_at_right b (f : map_at_right b) :=
MapForRight f (erefl (s' b)).
Definition unify_map_at_both a b (f : map_at_both a b) :=
MapForBoth f (erefl (s a)) (erefl (s' b)).
Structure wrapped := Wrap {unwrap : mapUUV}.
Definition wrap (f : map_class) := Wrap f.
End bilinear.
End Bilinear.
Notation "{ 'bilinear' U -> V -> W | s & t }" :=
(@Bilinear.type _ U%type V%type W%type s t)
(at level 0, U at level 98, V at level 98, W at level 99,
format "{ 'bilinear' U -> V -> W | s & t }") : ring_scope.
Notation "{ 'bilinear' U -> V -> W | s }" :=
({bilinear U → V → W | s.1 & s.2})
(at level 0, U at level 98, V at level 98, W at level 99,
format "{ 'bilinear' U -> V -> W | s }") : ring_scope.
Notation "{ 'bilinear' U -> V -> W }" := {bilinear U → V → W | *:%R & *:%R}
(at level 0, U at level 98, V at level 98, W at level 99,
format "{ 'bilinear' U -> V -> W }") : ring_scope.
Notation "{ 'biscalar' U }" := {bilinear U%type → U%type → _ | *%R & *%R}
(at level 0, format "{ 'biscalar' U }") : ring_scope.
End BilinearExports.
Export BilinearExports.
#[non_forgetful_inheritance]
HB.instance Definition _ (R : ringType) (U U' : lmodType R) (V : zmodType)
(s : R → V → V) (s' : R → V → V)
(f : {bilinear U → U' → V | s & s'}) (u : U)
:= @GRing.isAdditive.Build U' V (f u) (@additiver_subproof _ _ _ _ _ _ f u).
#[non_forgetful_inheritance]
HB.instance Definition _ (R : ringType) (U U' : lmodType R) (V : zmodType)
(s : R → V → V) (s' : R → V → V) (f : @bilinear R U U' V s s') (u : U)
:= @GRing.isScalable.Build _ _ _ _ (f u) (@linearr_subproof _ _ _ _ _ _ f u).
Section applyr.
Variables (R : ringType) (U U' : lmodType R) (V : zmodType)
(s s' : R → V → V).
Definition applyr_head t (f : U → U' → V) u v := let: tt := t in f v u.
End applyr.
Notation applyr := (applyr_head tt).
Coercion Bilinear.map_for_left_map : Bilinear.map_for_left >-> Bilinear.type.
Coercion Bilinear.map_for_right_map : Bilinear.map_for_right >-> Bilinear.type.
Coercion Bilinear.map_for_both_map : Bilinear.map_for_both >-> Bilinear.type.
Coercion Bilinear.unify_map_at_left : Bilinear.map_at_left >-> Bilinear.map_for_left.
Coercion Bilinear.unify_map_at_right : Bilinear.map_at_right >-> Bilinear.map_for_right.
Coercion Bilinear.unify_map_at_both : Bilinear.map_at_both >-> Bilinear.map_for_both.
Canonical Bilinear.unify_map_at_left.
Canonical Bilinear.unify_map_at_right.
Canonical Bilinear.unify_map_at_both.
Coercion Bilinear.unwrap : Bilinear.wrapped >-> Bilinear.type.
Coercion Bilinear.wrap : Bilinear.map_class >-> Bilinear.wrapped.
Canonical Bilinear.wrap.
Section BilinearTheory.
Variable R : ringType.
Section GenericProperties.
Variables (U U' : lmodType R) (V : zmodType) (s : R → V → V) (s' : R → V → V).
Variable f : {bilinear U → U' → V | s & s'}.
Section GenericPropertiesr.
Variable z : U.
#[local, non_forgetful_inheritance]
HB.instance Definition _ :=
GRing.isAdditive.Build _ _ (f z) (@additiver_subproof _ _ _ _ _ _ f z).
#[local, non_forgetful_inheritance]
HB.instance Definition _ :=
GRing.isScalable.Build _ _ _ _ (f z) (@linearr_subproof _ _ _ _ _ _ f z).
Lemma linear0r : f z 0 = 0.
Lemma linearNr : {morph f z : x / - x}.
Lemma linearDr : {morph f z : x y / x + y}.
Lemma linearBr : {morph f z : x y / x - y}.
Lemma linearMnr n : {morph f z : x / x *+ n}.
Lemma linearMNnr n : {morph f z : x / x *- n}.
Lemma linear_sumr I r (P : pred I) E :
f z (\sum_(i <- r | P i) E i) = \sum_(i <- r | P i) f z (E i).
Lemma linearZr_LR : scalable_for s' (f z).
Lemma linearPr a : {morph f z : u v / a *: u + v >-> s' a u + v}.
End GenericPropertiesr.
Lemma applyrE x : applyr f x =1 f^~ x.
Section GenericPropertiesl.
Variable z : U'.
Lemma linear0l : f 0 z = 0.
Lemma linearNl : {morph f^~ z : x / - x}.
Lemma linearDl : {morph f^~ z : x y / x + y}.
Lemma linearBl : {morph f^~ z : x y / x - y}.
Lemma linearMnl n : {morph f^~ z : x / x *+ n}.
Lemma linearMNnl n : {morph f^~ z : x / x *- n}.
Lemma linear_sumlz I r (P : pred I) E :
f (\sum_(i <- r | P i) E i) z = \sum_(i <- r | P i) f (E i) z.
Lemma linearZl_LR : scalable_for s (f ^~ z).
Lemma linearPl a : {morph f^~ z : u v / a *: u + v >-> s a u + v}.
End GenericPropertiesl.
End GenericProperties.
Section BidirectionalLinearZ.
Variables (U U' : lmodType R) (V : zmodType) (s s' : R → V → V).
Variables (S : ringType) (h : GRing.Scale.law S V) (h' : GRing.Scale.law S V).
Lemma linearZl z (c : S) (a : R) (h_c := h c)
(f : Bilinear.map_for_left U U' s s' a h_c) u :
f (a *: u) z = h_c (Bilinear.wrap f u z).
Lemma linearZr z c' b (h'_c' := h' c')
(f : Bilinear.map_for_right U U' s s' b h'_c') u :
f z (b *: u) = h'_c' (Bilinear.wrap f z u).
Lemma linearZlr c c' a b (h_c := h c) (h'_c' := h' c')
(f : Bilinear.map_for_both U U' s s' a b h_c h'_c') u v :
f (a *: u) (b *: v) = h_c (h'_c' (Bilinear.wrap f u v)).
Lemma linearZrl c c' a b (h_c := h c) (h'_c' := h' c')
(f : Bilinear.map_for_both U U' s s' a b h_c h'_c') u v :
f (a *: u) (b *: v) = h'_c' (h_c (Bilinear.wrap f u v)).
End BidirectionalLinearZ.
End BilinearTheory.
TODO Canonical rev_mulmx (R : ringType) m n p := [revop mulmxr of @mulmx R m n p]. Canonical mulmx_bilinear (R : comRingType) m n p := [bilinear of @mulmx R m n p].
Lemma mulmx_is_bilinear (R : comRingType) m n p : bilinear_for
(GRing.Scale.Law.clone _ _ *:%R _) (GRing.Scale.Law.clone _ _ *:%R _)
(@mulmx R m n p).
Section BilinearForms.
Variables (R : fieldType) (theta : {rmorphism R → R}).
Variables (n : nat) (M : 'M[R]_n).
Implicit Types (a b : R) (u v : 'rV[R]_n) (N P Q : 'M[R]_n).
Definition form u v := (u ×m M ×m (v ^t theta)) 0 0.
Local Notation "''[' u , v ]" := (form u%R v%R) : ring_scope.
Local Notation "''[' u ]" := '[u, u] : ring_scope.
Lemma form0l u : '[0, u] = 0.
Lemma form0r u : '[u, 0] = 0.
Lemma formDl u v w : '[u + v, w] = '[u, w] + '[v, w].
Lemma formDr u v w : '[u, v + w] = '[u, v] + '[u, w].
Lemma formZr a u v : '[u, a *: v] = theta a × '[u, v].
Lemma formZl a u v : '[a *: u, v] = a × '[u, v].
Lemma formNl u v : '[- u, v] = - '[u, v].
Lemma formNr u v : '[u, - v] = - '[u, v].
Lemma formee i j : '['e_i, 'e_j] = M i j.
Lemma form0_eq0 : M = 0 → ∀ u v, '[u, v] = 0.
End BilinearForms.
Notation "{ 'hermitian' U 'for' eps & theta }" := (@Hermitian.type _ U eps theta)
(at level 0, format "{ 'hermitian' U 'for' eps & theta }") : ring_scope.
duplicate to trick HB
#[non_forgetful_inheritance]
HB.instance Definition _ (R : ringType) (U : lmodType R)
(eps : bool) (theta : R → R) (f : {hermitian U for eps & theta}) (u : U) :=
@GRing.isAdditive.Build _ _ (f u) (@additiver_subproof _ _ _ _ _ _ f u).
#[non_forgetful_inheritance]
HB.instance Definition _ (R : ringType) (U : lmodType R)
(eps : bool) (theta : R → R) (f : {hermitian U for eps & theta}) (u : U) :=
@GRing.isScalable.Build _ _ _ _ (f u) (@linearr_subproof _ _ _ _ _ _ f u).
Variables (R : ringType) (U : lmodType R) (eps : bool) (theta : R -> R). Implicit Types phU : phant U. Local Coercion GRing.Scale.op : GRing.Scale.law >-> Funclass. Definition axiom (f : U -> U -> R) := forall x y : U, f x y = (-1) ^+ eps * theta (f y x). Record class_of (f : U -> U -> R) : Prop := Class { base : Bilinear.class_of ( *%R) (theta \; *%R) f; mixin : axiom f }. Canonical additiver (u : U) := Additive (base class u). Canonical linearr (u : U) := Linear (base class u). Canonical additivel (u' : U) := @GRing.Additive.Pack _ _ (Phant (U -> R)) (applyr cF u') (Bilinear.basel (base class) u'). Canonical linearl (u' : U) := @GRing.Linear.Pack _ _ _ _ (Phant (U -> R)) (applyr cF u') (Bilinear.basel (base class) u'). Canonical bilinear := @Bilinear.Pack _ _ _ _ _ _ (Phant (U -> U -> R)) cF (base class). Module Exports. Notation "{ 'hermitian' U 'for' eps & theta }" := (map eps theta (Phant U)) (at level 0, format "{ 'hermitian' U 'for' eps & theta }") : ring_scope. Coercion base : class_of >-> bilmorphism_for. Coercion apply : map >-> Funclass. Notation " [ 'hermitian' 'of' f 'as' g ]" := (@clone _ _ _ _ _ _ f g _ idfun idfun) (at level 0, format " [ 'hermitian' 'of' f 'as' g ]") : form_scope. Notation " [ 'hermitian' 'of' f ]" := (@clone _ _ _ _ _ _ f f _ idfun idfun) (at level 0, format " [ 'hermitian' 'of' f ]") : form_scope. Notation hermitian_for := Hermitian.axiom. Notation Hermitian fM := (pack (Phant _) fM idfun). Canonical additiver. Canonical linearr. Canonical additivel. Canonical linearl. Canonical bilinear. Notation hermapplyr := (@applyr_head _ _ _ _ tt). End Exports. End Hermitian. Include Hermitian.Exports.
Definition orthomx {R : fieldType} (theta : R → R) n m M (B : 'M_(m, n)) : 'M_n :=
kermx (M ×m (B ^t theta)).
Section Sesquilinear.
Variables (R : fieldType) (n : nat).
Implicit Types (a b : R) (u v : 'rV[R]_n) (N P Q : 'M[R]_n).
Section Def.
Variable eps_theta : bool × {rmorphism R → R}.
Definition sesqui :=
[qualify M : 'M_n | M == ((-1) ^+ eps_theta.1) *: M ^t eps_theta.2].
Fact sesqui_key : pred_key sesqui.
Canonical sesqui_keyed := KeyedQualifier sesqui_key.
End Def.
Local Notation "eps_theta .-sesqui" := (sesqui eps_theta).
Variables (eps : bool) (theta : {rmorphism R → R}) (M : 'M[R]_n).
Local Notation "''[' u , v ]" := (form theta M u%R v%R) : ring_scope.
Local Notation "''[' u ]" := '[u, u] : ring_scope.
Lemma sesquiE : (M \is (eps, theta).-sesqui) = (M == (-1) ^+ eps *: M ^t theta).
Lemma sesquiP : reflect (M = (-1) ^+ eps *: M ^t theta)
(M \is (eps, theta).-sesqui).
Hypotheses (thetaK : involutive theta) (M_sesqui : M \is (eps, theta).-sesqui).
Lemma trmx_sesqui : M^T = (-1) ^+ eps *: M ^ theta.
Lemma maptrmx_sesqui : M^t theta = (-1) ^+ eps *: M.
Lemma formC u v : '[u, v] = (-1) ^+ eps × theta '[v, u].
Lemma form_eq0C u v : ('[u, v] == 0) = ('[v, u] == 0).
Definition ortho m (B : 'M_(m, n)) := orthomx theta M B.
Local Notation "B ^_|_" := (ortho B) : ring_scope.
Local Notation "A '_|_ B" := (A%MS ≤ B^_|_)%MS : ring_scope.
Lemma normalE u v : (u '_|_ v) = ('[u, v] == 0).
Lemma form_eq0P {u v} : reflect ('[u, v] = 0) (u '_|_ v).
Lemma normalP p q (A : 'M_(p, n)) (B :'M_(q, n)) :
reflect (∀ (u v : 'rV_n), (u ≤ A)%MS → (v ≤ B)%MS → u '_|_ v)
(A '_|_ B).
Lemma normalC p q (A : 'M_(p, n)) (B : 'M_(q, n)) : (A '_|_ B) = (B '_|_ A).
Lemma normal_ortho_mx p (A : 'M_(p, n)) : ((A^_|_) '_|_ A).
Lemma normal_mx_ortho p (A : 'M_(p, n)) : (A '_|_ (A^_|_)).
Lemma rank_normal u : (\rank (u ^_|_) ≥ n.-1)%N.
Definition rad := 1%:M^_|_.
Lemma rad_ker : rad = kermx M.
Pythagoras
Theorem formDd u v : u '_|_ v → '[u + v] = '[u] + '[v].
Lemma formZ a u : '[a *: u]= (a × theta a) × '[u].
Lemma formN u : '[- u] = '[u].
Lemma form_sign m u : '[(-1) ^+ m *: u] = '[u].
Lemma formD u v : let d := '[u, v] in
'[u + v] = '[u] + '[v] + (d + (-1) ^+ eps × theta d).
Lemma formB u v : let d := '[u, v] in
'[u - v] = '[u] + '[v] - (d + (-1) ^+ eps × theta d).
Lemma formBd u v : u '_|_ v → '[u - v] = '[u] + '[v].
Lemma formJ u v : ' [u ^ theta, v ^ theta] = (-1) ^+ eps * theta ' [u, v]. Proof. rewrite {1}/form -map_trmx -map_mx_comp (@eq_map_mx _ _ _ _ _ id) ?map_mx_id //. set x := (_ *m _); have -> : x 0 0 = theta ((x^t theta) 0 0) by rewrite !mxE. rewrite !trmx_mul trmxK map_trmx mulmxA !map_mxM. rewrite maptrmx_sesqui -!scalemxAr -scalemxAl mxE rmorphM rmorph_sign. Lemma formJ u : ' [u ^ theta] = (-1) ^+ eps * ' [u]. Proof. rewrite {1}/form -map_trmx -map_mx_comp (@eq_map_mx _ _ _ _ _ id) ?map_mx_id //. set x := (_ *m _); have -> : x 0 0 = theta ((x^t theta) 0 0) by rewrite !mxE. rewrite !trmx_mul trmxK map_trmx mulmxA !map_mxM. rewrite maptrmx_sesqui -!scalemxAr -scalemxAl mxE rmorphM rmorph_sign. rewrite !map_mxM. rewrite -map_mx_comp eq_map_mx_id //. !linearZr_LR /=. linearZ. linearZl. rewrite trmx_sesqui. rewrite mapmx. rewrite map apply/matrixP. rewrite formC. Proof. by rewrite cfdot_conjC geC0_conj // cfnorm_ge0. Qed. Lemma cfCauchySchwarz u v : `|' [u, v]| ^+ 2 <= ' [u] * ' [v] ?= iff ~~ free (u :: v). Proof. rewrite free_cons span_seq1 seq1_free -negb_or negbK orbC. have [-> | nz_v] /= := altP (v =P 0). by apply/lerifP; rewrite !cfdot0r normCK mul0r mulr0. without loss ou: u / ' [u, v] = 0. move=> IHo; pose a := ' [u, v] / ' [v]; pose u1 := u - a *: v. have ou: ' [u1, v] = 0. by rewrite cfdotBl cfdotZl divfK ?cfnorm_eq0 ?subrr. rewrite (canRL (subrK _) (erefl u1)) rpredDr ?rpredZ ?memv_line //. rewrite cfdotDl ou add0r cfdotZl normrM (ger0_norm (cfnorm_ge0 _)). rewrite exprMn mulrA -cfnormZ cfnormDd; last by rewrite cfdotZr ou mulr0. by have:= IHo _ ou; rewrite mulrDl -lerif_subLR subrr ou normCK mul0r. rewrite ou normCK mul0r; split; first by rewrite mulr_ge0 ?cfnorm_ge0. rewrite eq_sym mulf_eq0 orbC cfnorm_eq0 (negPf nz_v) /=. apply/idP/idP=> [|/vlineP[a {2}-> ]#]; last by rewrite cfdotZr ou mulr0. by rewrite cfnorm_eq0 => /eqP->; apply: rpred0. Qed.
End Sesquilinear.
Notation "eps_theta .-sesqui" := (sesqui _ eps_theta) : ring_scope.
Notation symmetric_form := (false, idfun).-sesqui.
Notation skew := (true, idfun).-sesqui.
Notation hermitian := (false, @Num.conj_op _).-sesqui.
Notation "{ 'dot' U 'for' theta }" := (@Dot.type _ U theta)
(at level 0, format "{ 'dot' U 'for' theta }") : ring_scope.
duplicate to trick HB
#[non_forgetful_inheritance]
HB.instance Definition _ (R : numDomainType) (U : lmodType R)
(theta : R → R) (f : {dot U for theta}) (u : U) :=
@GRing.isAdditive.Build _ _ (f u) (@additiver_subproof _ _ _ _ _ _ f u).
#[non_forgetful_inheritance]
HB.instance Definition _ (R : numDomainType) (U : lmodType R)
(theta : R → R) (f : {dot U for theta}) (u : U) :=
@GRing.isScalable.Build _ _ _ _ (f u) (@linearr_subproof _ _ _ _ _ _ f u).
Notation "{ 'dot' U 'for' theta }" := (map theta (Phant U)) (at level 0, format "{ 'dot' U 'for' theta }") : ring_scope. Coercion base : class_of >-> Hermitian.class_of. Coercion apply : map >-> Funclass. Notation " [ 'dot' 'of' f 'as' g ]" := (@clone _ _ _ _ _ f g _ idfun idfun) (at level 0, format " [ 'dot' 'of' f 'as' g ]") : form_scope. Notation " [ 'dot' 'of' f ]" := (@clone _ _ _ _ _ f f _ idfun idfun) (at level 0, format " [ 'dot' 'of' f ]") : form_scope. Notation Dot fM := (pack fM idfun). Notation is_dot := Dot.axiom.
Notation "{ 'symmetric' U }" := ({hermitian U for false & idfun})
(at level 0, format "{ 'symmetric' U }") : ring_scope.
Notation "{ 'skew_symmetric' U }" := ({hermitian U for true & idfun})
(at level 0, format "{ 'skew_symmetric' U }") : ring_scope.
Notation "{ 'hermitian_sym' U 'for' theta }" := ({hermitian U for false & theta})
(at level 0, format "{ 'hermitian_sym' U 'for' theta }") : ring_scope.
Definition is_skew (R : ringType) (eps : bool) (theta : R → R)
(U : lmodType R) (form : {hermitian U for eps & theta}) :=
(eps = true) ∧ (theta =1 id).
Definition is_sym (R : ringType) (eps : bool) (theta : R → R)
(U : lmodType R) (form : {hermitian U for eps & theta}) :=
(eps = false) ∧ (theta =1 id).
Definition is_hermsym (R : ringType) (eps : bool) (theta : R → R)
(U : lmodType R) (form : {hermitian U for eps & theta}) :=
(eps = false).
Section HermitianModuleTheory.
Variables (R : ringType) (eps : bool) (theta : {rmorphism R → R}).
Variables (U : lmodType R) (form : {hermitian U for eps & theta}).
Local Notation "''[' u , v ]" := (form u%R v%R) : ring_scope.
Local Notation "''[' u ]" := '[u, u]%R : ring_scope.
Lemma hermC u v : '[u, v] = (-1) ^+ eps × theta '[v, u].
Lemma hnormN u : '[- u] = '[u].
Lemma hnorm_sign n u : '[(-1) ^+ n *: u] = '[u].
Lemma hnormD u v :
let d := '[u, v] in '[u + v] = '[u] + '[v] + (d + (-1) ^+ eps × theta d).
Lemma hnormB u v :
let d := '[u, v] in '[u - v] = '[u] + '[v] - (d + (-1) ^+ eps × theta d).
Lemma hnormDd u v : '[u, v] = 0 → '[u + v] = '[u] + '[v].
Lemma hnormBd u v : '[u, v] = 0 → '[u - v] = '[u] + '[v].
Local Notation "u '_|_ v" := ('[u, v] == 0) : ring_scope.
Definition ortho_rec (s1 s2 : seq U) :=
all [pred u | all [pred v | u '_|_ v] s2] s1.
Fixpoint pair_ortho_rec (s : seq U) :=
if s is v :: s' then ortho_rec [:: v] s' && pair_ortho_rec s' else true.
We exclude 0 from pairwise orthogonal sets.
Definition pairwise_orthogonal s := (0 \notin s) && pair_ortho_rec s.
Definition orthogonal s1 s2 := (@ortho_rec s1 s2).
Arguments orthogonal : simpl never.
Lemma orthogonal_cons u us vs :
orthogonal (u :: us) vs = orthogonal [:: u] vs && orthogonal us vs.
Definition orthonormal s := all [pred v | '[v] == 1] s && pair_ortho_rec s.
Lemma orthonormal_not0 S : orthonormal S → 0 \notin S.
Lemma orthonormalE S :
orthonormal S = all [pred phi | '[phi] == 1] S && pairwise_orthogonal S.
Lemma orthonormal_orthogonal S : orthonormal S → pairwise_orthogonal S.
End HermitianModuleTheory.
Arguments orthogonal {R eps theta U} form s1 s2.
Arguments pairwise_orthogonal {R eps theta U} form s.
Arguments orthonormal {R eps theta U} form s.
Section HermitianIsometry.
Variables (R : ringType) (eps : bool) (theta : {rmorphism R → R}).
Variables (U1 U2 : lmodType R) (form1 : {hermitian U1 for eps & theta})
(form2 : {hermitian U2 for eps & theta}).
Local Notation "''[' u , v ]_1" := (form1 u%R v%R) : ring_scope.
Local Notation "''[' u , v ]_2" := (form2 u%R v%R) : ring_scope.
Local Notation "''[' u ]_1" := (form1 u%R u%R) : ring_scope.
Local Notation "''[' u ]_2" := (form2 u%R u%R): ring_scope.
Definition isometry tau := ∀ u v, form1 (tau u) (tau v) = form2 u%R v%R.
Definition isometry_from_to mD tau mR :=
prop_in2 mD (inPhantom (isometry tau)) ∧
prop_in1 mD (inPhantom (∀ u, in_mem (tau u) mR)).
Local Notation "{ 'in' D , 'isometry' tau , 'to' R }" :=
(isometry_from_to (mem D) tau (mem R))
(at level 0, format "{ 'in' D , 'isometry' tau , 'to' R }")
: type_scope.
End HermitianIsometry.
Section HermitianVectTheory.
Variables (R : fieldType) (eps : bool) (theta : {rmorphism R → R}).
Variable (U : lmodType R) (form : {hermitian U for eps & theta}).
Local Notation "''[' u , v ]" := (form u%R v%R) : ring_scope.
Local Notation "''[' u ]" := '[u, u]%R : ring_scope.
Lemma herm_eq0C u v : ('[u, v] == 0) = ('[v, u] == 0).
End HermitianVectTheory.
Section HermitianFinVectTheory.
Variables (F : fieldType) (eps : bool) (theta : {rmorphism F → F}).
Variables (vT : vectType F) (form : {hermitian vT for eps & theta}).
Let n := \dim {:vT}.
Implicit Types (u v : vT) (U V : {vspace vT}).
Local Notation "''[' u , v ]" := (form u%R v%R) : ring_scope.
Local Notation "''[' u ]" := '[u, u]%R : ring_scope.
Let alpha v := (linfun (applyr form v : vT → F^o)).
Definition orthov V := (\bigcap_(i < \dim V) lker (alpha (vbasis V)`_i))%VS.
Local Notation "U '_|_ V" := (U ≤ orthov V)%VS : vspace_scope.
Lemma mem_orthovPn V u : reflect (exists2 v, v \in V & '[u, v] != 0) (u \notin orthov V).
Lemma mem_orthovP V u : reflect {in V, ∀ v, '[u, v] = 0} (u \in orthov V).
Lemma orthov1E u : orthov <[u]> = lker (alpha u).
Lemma orthovP U V : reflect {in U & V, ∀ u v, '[u, v] = 0} (U '_|_ V)%VS.
Lemma orthov_sym U V : (U '_|_ V)%VS = (V '_|_ U)%VS.
Lemma mem_orthov1 v u : (u \in orthov <[v]>) = ('[u, v] == 0).
Lemma orthov11 u v : (<[u]> '_|_ <[v]>)%VS = ('[u, v] == 0).
Lemma mem_orthov1_sym v u : (u \in orthov <[v]>) = (v \in orthov <[u]>).
Lemma orthov0 : orthov 0 = fullv.
Lemma mem_orthov_sym V u : (u \in orthov V) = (V ≤ orthov <[u]>)%VS.
Lemma leq_dim_orthov1 u V : ((\dim V).-1 ≤ \dim (V :&: orthov <[u]>))%N.
Lemma dim_img_form_eq1 u V : u \notin orthov V → \dim (alpha u @: V)%VS = 1%N.
Lemma eq_dim_orthov1 u V : u \notin orthov V → (\dim V).-1 = \dim (V :&: orthov <[u]>).
Lemma dim_img_form_eq0 u V : u \in orthov V → \dim (alpha u @: V)%VS = 0%N.
Lemma neq_dim_orthov1 u V : (\dim V > 0)%N →
u \in orthov V → ((\dim V).-1 < \dim (V :&: orthov <[u]>))%N.
Lemma leqif_dim_orthov1 u V : (\dim V > 0)%N →
((\dim V).-1 ≤ \dim (V :&: orthov <[u]>) ?= iff (u \notin orthov V))%N.
Lemma leqif_dim_orthov1_full u : (n > 0)%N →
((\dim {:vT}).-1 ≤ \dim (orthov <[u]>) ?= iff (u \notin orthov fullv))%N.
Link between orthov and orthovgonality of sequences
Lemma orthogonal1P u v : reflect ('[u, v] = 0) (orthogonal form [:: u] [:: v]).
Lemma orthogonalP us vs :
reflect {in us & vs, ∀ u v, '[u, v] = 0} (orthogonal form us vs).
Lemma orthogonal_oppr S R : orthogonal form S (map -%R R) = orthogonal form S R.
Lemma orthogonalE us vs : (orthogonal form us vs) = (<<us>> '_|_ <<vs>>)%VS.
Lemma orthovE U V : (U '_|_ V)%VS = orthogonal form (vbasis U) (vbasis V).
Notation radv := (orthov fullv).
Lemma orthoDv U V W : (U + V '_|_ W)%VS = (U '_|_ W)%VS && (V '_|_ W)%VS.
Lemma orthovD U V W : (U '_|_ V + W)%VS = (U '_|_ V)%VS && (U '_|_ W)%VS.
Definition nondegenerate := radv == 0%VS.
Definition is_symplectic := [/\ nondegenerate, is_skew form &
2 \in [char F] → ∀ u, '[u, u] = 0].
Definition is_orthogonal := [/\ nondegenerate, is_sym form &
2 \in [char F] → ∀ u, '[u, u] = 0].
Definition is_unitary := nondegenerate ∧ (is_hermsym form).
End HermitianFinVectTheory.
Arguments orthogonalP {F eps theta vT form us vs}.
Arguments orthovP {F eps theta vT form U V}.
Arguments mem_orthovPn {F eps theta vT form V u}.
Arguments mem_orthovP {F eps theta vT form V u}.
Section DotVectTheory.
Variables (C : numClosedFieldType).
Variable (U : lmodType C) (form : {dot U for conjC}).
Local Notation "''[' u , v ]" := (form u%R v%R) : ring_scope.
Local Notation "''[' u ]" := '[u, u]%R : ring_scope.
Lemma dnorm_geiff0 u : 0 ≤ '[u] ?= iff (u == 0).
Lemma dnorm_ge0 u : 0 ≤ '[u].
Lemma dnorm_eq0 u : ('[u] == 0) = (u == 0).
Lemma dnorm_gt0 u : (0 < '[u]) = (u != 0).
Lemma sqrt_dnorm_ge0 u : 0 ≤ sqrtC '[u].
Lemma sqrt_dnorm_eq0 u : (sqrtC '[u] == 0) = (u == 0).
Lemma sqrt_dnorm_gt0 u : (sqrtC '[u] > 0) = (u != 0).
Lemma dnormZ a u : '[a *: u]= `|a| ^+ 2 × '[u].
Lemma dnormD u v : let d := '[u, v] in '[u + v] = '[u] + '[v] + (d + d^*).
Lemma dnormB u v : let d := '[u, v] in '[u - v] = '[u] + '[v] - (d + d^*).
End DotVectTheory.
#[global]
Hint Extern 0 (is_true (0 ≤ Dot.sort _ _ _
(* NB: This Hint is assuming ^*, a more precise pattern would be welcome *)))
⇒ apply: dnorm_ge0 : core.
Section HermitianTheory.
Variables (C : numClosedFieldType) (eps : bool) (theta : {rmorphism C → C}).
Variable (U : lmodType C) (form : {dot U for conjC}).
Local Notation "''[' u , v ]" := (form u%R v%R) : ring_scope.
Local Notation "''[' u ]" := '[u, u]%R : ring_scope.
Lemma pairwise_orthogonalP S :
reflect (uniq (0 :: S)
∧ {in S &, ∀ phi psi, phi != psi → '[phi, psi] = 0})
(pairwise_orthogonal form S).
Lemma pairwise_orthogonal_cat R S :
pairwise_orthogonal form (R ++ S) =
[&& pairwise_orthogonal form R, pairwise_orthogonal form S & orthogonal form R S].
Lemma orthonormal_cat R S :
orthonormal form (R ++ S) =
[&& orthonormal form R, orthonormal form S & orthogonal form R S].
Lemma orthonormalP S :
reflect (uniq S ∧ {in S &, ∀ phi psi, '[phi, psi] = (phi == psi)%:R})
(orthonormal form S).
Lemma sub_orthonormal S1 S2 :
{subset S1 ≤ S2} → uniq S1 → orthonormal form S2 → orthonormal form S1.
Lemma orthonormal2P phi psi :
reflect [/\ '[phi, psi] = 0, '[phi] = 1 & '[psi] = 1]
(orthonormal form [:: phi; psi]).
End HermitianTheory.
Section DotFinVectTheory.
Variable C : numClosedFieldType.
Variables (U : vectType C) (form : {dot U for conjC}).
Local Notation "''[' u , v ]" := (form u%R v%R) : ring_scope.
Local Notation "''[' u ]" := '[u, u]%R : ring_scope.
Lemma sub_pairwise_orthogonal S1 S2 :
{subset S1 ≤ S2} → uniq S1 →
pairwise_orthogonal form S2 → pairwise_orthogonal form S1.
Lemma orthogonal_free S : pairwise_orthogonal form S → free S.
Lemma filter_pairwise_orthogonal S p :
pairwise_orthogonal form S → pairwise_orthogonal form (filter p S).
Lemma orthonormal_free S : orthonormal form S → free S.
Theorem CauchySchwarz (u v : U) :
`|'[u, v]| ^+ 2 ≤ '[u] × '[v] ?= iff ~~ free [:: u; v].
Lemma CauchySchwarz_sqrt u v :
`|'[u, v]| ≤ sqrtC '[u] × sqrtC '[v] ?= iff ~~ free [:: u; v].
Lemma orthoP phi psi : reflect ('[phi, psi] = 0) (orthogonal form [:: phi] [:: psi]).
Lemma orthoPl phi S :
reflect {in S, ∀ psi, '[phi, psi] = 0} (orthogonal form [:: phi] S).
Arguments orthoPl {phi S}.
Lemma orthogonal_sym : symmetric (orthogonal form).
Lemma orthoPr S psi :
reflect {in S, ∀ phi, '[phi, psi] = 0} (orthogonal form S [:: psi]).
Lemma orthogonal_catl R1 R2 S :
orthogonal form (R1 ++ R2) S = orthogonal form R1 S && orthogonal form R2 S.
Lemma orthogonal_catr R S1 S2 :
orthogonal form R (S1 ++ S2) = orthogonal form R S1 && orthogonal form R S2.
Lemma eq_pairwise_orthogonal R S :
perm_eq R S → pairwise_orthogonal form R = pairwise_orthogonal form S.
Lemma eq_orthonormal S0 S : perm_eq S0 S → orthonormal form S0 = orthonormal form S.
Lemma orthogonal_oppl S R : orthogonal form (map -%R S) R = orthogonal form S R.
Lemma triangle_lerif u v :
sqrtC '[u + v] ≤ sqrtC '[u] + sqrtC '[v]
?= iff ~~ free [:: u; v] && (0 ≤ coord [tuple v] 0 u).
Lemma span_orthogonal S1 S2 phi1 phi2 :
orthogonal form S1 S2 → phi1 \in <<S1>>%VS → phi2 \in <<S2>>%VS →
'[phi1, phi2] = 0.
Lemma orthogonal_split S beta :
{X : U & X \in <<S>>%VS &
{Y :U | [/\ beta = X + Y, '[X, Y] = 0 & orthogonal form [:: Y] S]}}.
End DotFinVectTheory.
Arguments orthoP {C U form phi psi}.
Arguments pairwise_orthogonalP {C U form S}.
Arguments orthonormalP {C U form S}.
Arguments orthoPl {C U form phi S}.
Arguments orthoPr {C U form S psi}.
Section BuildIsometries.
Variables (C : numClosedFieldType) (U U1 U2 : vectType C).
Variables (form : {dot U for conjC}) (form1 : {dot U1 for conjC})
(form2 : {dot U2 for conjC}).
Definition normf1 := fun u ⇒ form1 u u.
Definition normf2 := fun u ⇒ form2 u u.
Lemma isometry_of_dnorm S tauS :
pairwise_orthogonal form1 S → pairwise_orthogonal form2 tauS →
map normf2 tauS = map normf1 S →
{tau : {linear U1 → U2} | map tau S = tauS
& {in <<S>>%VS &, isometry form2 form1 tau}}.
Lemma isometry_of_free S f :
free S → {in S &, isometry form2 form1 f} →
{tau : {linear U1 → U2} |
{in S, tau =1 f} & {in <<S>>%VS &, isometry form2 form1 tau}}.
Lemma isometry_raddf_inj (tau : {additive U1 → U2}) :
{in U1 &, isometry form2 form1 tau} →
{in U1 &, ∀ u v, u - v \in U1} →
{in U1 &, injective tau}.
End BuildIsometries.
Section MatrixForms.
Variables (R : fieldType) (n : nat).
Implicit Types (a b : R) (u v : 'rV[R]_n) (M N P Q : 'M[R]_n).
Section Def.
Variable theta : R → R.
Definition form_of_matrix m M (U V : 'M_(m, n)) := \tr (U ×m M ×m (V ^t theta)).
Definition matrix_of_form (form : 'rV[R]_n → 'rV[R]_n → R) : 'M[R]_n :=
\matrix_(i, j) form 'e_i 'e_j.
Implicit Type form : {bilinear 'rV[R]_n → 'rV[R]_n → R | *%R & theta \; *%R}.
Lemma matrix_of_formE form i j : matrix_of_form form i j = form 'e_i 'e_j.
End Def.
Section FormOfMatrix.
Variables (m : nat) (M : 'M[R]_n).
Implicit Types (U V : 'M[R]_(m, n)).
Variables (theta : {rmorphism R → R}).
Local Notation "''[' U , V ]" := (form_of_matrix theta M U%R V%R) : ring_scope.
Local Notation "''[' U ]" := '[U, U]%R : ring_scope.
Let form_of_matrix_is_linear U :
linear_for (theta \; *%R) (form_of_matrix theta M U).
Definition form_of_matrixr U := (form_of_matrix theta M)^~U.
Let form_of_matrixr_is_linear U : linear_for *%R (form_of_matrixr U).
TODO Canonical form_of_matrixr_rev := [revop form_of_matrixr of form_of_matrix theta M].
Lemma form_of_matrix_is_bilinear :
bilinear_for
(GRing.Scale.Law.clone _ _ ( *%R ) _) (GRing.Scale.Law.clone _ _ (theta \; *%R ) _)
(@form_of_matrix theta m M).
Canonical form_of_matrix_is_bilinear := [the @bilinear _ _ _ _ of form_of_matrix theta M].
End FormOfMatrix.
Section FormOfMatrix1.
Variables (M : 'M[R]_n).
Variables (theta : {rmorphism R → R}).
Local Notation "''[' u , v ]" := (form_of_matrix theta M u%R v%R) : ring_scope.
Local Notation "''[' u ]" := '[u, u]%R : ring_scope.
Lemma rV_formee i j : '['e_i :'rV__, 'e_j] = M i j.
Lemma form_of_matrixK : matrix_of_form (form_of_matrix theta M) = M.
Lemma rV_form0_eq0 : M = 0 → ∀ u v, '[u, v] = 0.
End FormOfMatrix1.
Section MatrixOfForm.
Variable (theta : {rmorphism R → R}).
Variable form : {bilinear 'rV[R]_n → 'rV[R]_n → R | *%R & theta \; *%R}.
Lemma matrix_of_formK : form_of_matrix theta (matrix_of_form form) =2 form.
End MatrixOfForm.
Section HermitianMx.
Variable eps : bool.
Section HermitianMxDef.
Variable theta : R → R.
Definition hermitianmx :=
[qualify M : 'M_n | M == ((-1) ^+ eps) *: M ^t theta].
Fact hermitianmx_key : pred_key hermitianmx.
Canonical hermitianmx_keyed := KeyedQualifier hermitianmx_key.
Structure hermitian_matrix := HermitianMx {
mx_of_hermitian :> 'M[R]_n;
_ : mx_of_hermitian \is hermitianmx }.
Lemma is_hermitianmxE M :
(M \is hermitianmx) = (M == (-1) ^+ eps *: M ^t theta).
Lemma is_hermitianmxP M :
reflect (M = (-1) ^+ eps *: M ^t theta) (M \is hermitianmx).
Lemma hermitianmxE (M : hermitian_matrix) :
M = ((-1) ^+ eps) *: M ^t theta :> 'M__.
Lemma trmx_hermitian (M : hermitian_matrix) :
M^T = ((-1) ^+ eps) *: M ^ theta :> 'M__.
End HermitianMxDef.
Section HermitianMxTheory.
Variables (theta : involutive_rmorphism R) (M : hermitian_matrix theta).
Lemma maptrmx_hermitian : M^t theta = (-1) ^+ eps *: (M : 'M__).
Lemma form_of_matrix_is_hermitian m x y :
(@form_of_matrix theta m M) x y =
(-1) ^+ eps × theta ((@form_of_matrix theta m M) y x).
Local Notation "''[' u , v ]" := (form_of_matrix theta M u%R v%R) : ring_scope.
Local Notation "''[' u ]" := '[u, u]%R : ring_scope.
Local Notation "B ^!" := (orthomx theta M B) : matrix_set_scope.
Local Notation "A '_|_ B" := (A%MS ≤ B%MS^!)%MS : matrix_set_scope.
Lemma orthomxE u v : (u '_|_ v)%MS = ('[u, v] == 0).
Lemma hermmx_eq0P {u v} : reflect ('[u, v] = 0) (u '_|_ v)%MS.
Lemma orthomxP p q (A : 'M_(p, n)) (B :'M_(q, n)) :
reflect (∀ (u v : 'rV_n), u ≤ A → v ≤ B → u '_|_ v)%MS
(A '_|_ B)%MS.
Lemma orthomx_sym p q (A : 'M_(p, n)) (B :'M_(q, n)) :
(A '_|_ B)%MS = (B '_|_ A)%MS.
Lemma ortho_ortho_mx p (A : 'M_(p, n)) : (A^! '_|_ A)%MS.
Lemma ortho_mx_ortho p (A : 'M_(p, n)) : (A '_|_ A^!)%MS.
Lemma rank_orthomx u : (\rank (u ^!) ≥ n.-1)%N.
Local Notation radmx := (1%:M^!)%MS.
Lemma radmxE : radmx = kermx M.
Lemma orthoNmx k m (A : 'M[R]_(k, n)) (B : 'M[R]_(m, n)) :
((- A) '_|_ B)%MS = (A '_|_ B)%MS.
Lemma orthomxN k m (A : 'M[R]_(k, n)) (B : 'M[R]_(m, n)) :
(A '_|_ (- B))%MS = (A '_|_ B)%MS.
Lemma orthoDmx k m p (A : 'M[R]_(k, n)) (B : 'M[R]_(m, n)) (C : 'M[R]_(p, n)) :
(A + B '_|_ C)%MS = (A '_|_ C)%MS && (B '_|_ C)%MS.
Lemma orthomxD k m p (A : 'M[R]_(k, n)) (B : 'M[R]_(m, n)) (C : 'M[R]_(p, n)) :
(A '_|_ B + C)%MS = (A '_|_ B)%MS && (A '_|_ C)%MS.
Lemma orthoZmx p m a (A : 'M[R]_(p, n)) (B : 'M[R]_(m, n)) : a != 0 →
(a *: A '_|_ B)%MS = (A '_|_ B)%MS.
Lemma orthomxZ p m a (A : 'M[R]_(p, n)) (B : 'M[R]_(m, n)) : a != 0 →
(A '_|_ (a *: B))%MS = (A '_|_ B)%MS.
Lemma eqmx_ortho p m (A : 'M[R]_(p, n)) (B : 'M[R]_(m, n)) :
(A :=: B)%MS → (A^! :=: B^!)%MS.
Lemma genmx_ortho p (A : 'M[R]_(p, n)) : (<<A>>^! :=: A^!)%MS.
End HermitianMxTheory.
End HermitianMx.
End MatrixForms.
Notation symmetricmx := (hermitianmx _ false idfun).
Notation skewmx := (hermitianmx _ true idfun).
Notation hermsymmx := (hermitianmx _ false conjC).
Lemma hermitian1mx_subproof {C : numClosedFieldType} n : (1%:M : 'M[C]_n) \is hermsymmx.
Canonical hermitian1mx {C : numClosedFieldType} n :=
HermitianMx (@hermitian1mx_subproof C n).