diff options
| author | Cyril Cohen | 2020-01-03 14:45:53 +0100 |
|---|---|---|
| committer | GitHub | 2020-01-03 14:45:53 +0100 |
| commit | c7fa2a1444d450bcebdeea47800fef1436690b6d (patch) | |
| tree | e0cf42c9b4b8ad39ddec274a368e1f6800b9cc49 /mathcomp/character/mxabelem.v | |
| parent | a93a392121e8e02c6fdaa6c674dd90af8b12c28d (diff) | |
| parent | a06d61a8e226eeabc52f1a22e469dca1e6077065 (diff) | |
Merge pull request #443 from pi8027/eqVneq
Refactoring and linting proofs especially in polydiv.v
Diffstat (limited to 'mathcomp/character/mxabelem.v')
| -rw-r--r-- | mathcomp/character/mxabelem.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v index f5755a3..1c3fe0b 100644 --- a/mathcomp/character/mxabelem.v +++ b/mathcomp/character/mxabelem.v @@ -199,7 +199,7 @@ move=> linL; apply/eqP; rewrite eqEsubset sub_rowg_mx andbT. apply/subsetP=> v; rewrite inE genmxE => /submxP[u ->{v}]. rewrite mulmx_sum_row group_prod // => i _. rewrite rowK; move: (enum_val i) (enum_valP i) => v Lv. -case: (eqVneq (u 0 i) 0) => [->|]; first by rewrite scale0r group1. +have [->|] := eqVneq (u 0 i) 0; first by rewrite scale0r group1. by rewrite -unitfE => aP; rewrite ((actsP linL) (FinRing.Unit _ aP)) ?inE. Qed. |