diff options
| author | Cyril Cohen | 2020-11-09 01:06:18 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-09 01:06:18 +0100 |
| commit | 8b98bcedc4523e07e4fdc118159cf171366e952d (patch) | |
| tree | aa5fd79fd3938e2e529dd1142e77ecab283af244 /mathcomp/algebra/mxalgebra.v | |
| parent | c33309d4279c5d6483af54b54fe6aa326e289f9b (diff) | |
`comm(Cmx|_mxC)` -> `comm(_scalar_mx|_mx_scalar)`
Diffstat (limited to 'mathcomp/algebra/mxalgebra.v')
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index e65bc3c..7aa89b8 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -2291,7 +2291,7 @@ Lemma comm_mx_stable_eigenspace (f g : 'M[F]_n) a : comm_mx f g -> stablemx (eigenspace f a) g. Proof. move=> cfg; rewrite comm_mx_stable_ker//. -by apply/comm_mx_sym/comm_mxB => //; apply:comm_mxC. +by apply/comm_mx_sym/comm_mxB => //; apply:comm_mx_scalar. Qed. End Commutation. |