Skip to content

Adapt to https://github.com/math-comp/analysis/pull/1508 #106

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
proux01 merged 1 commit into from
Feb 28, 2025
Merged

Adapt to https://github.com/math-comp/analysis/pull/1508 #106

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions theory/kaplansky.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -173,12 +173,12 @@ constructor; rewrite ?unitmx_mul; last first.
rewrite -[M]hsubmxK -/A1 -/A2 -[_ *m P1 *m _]mulmxA (mul_mx_row _ A1) -!mulmxA.
rewrite [row_mx (P1 *m A1) _ *m (_ *m _)]mulmxA mul_row_block ?simplmx !mulmxA.
have -> : lift0_mx L1 *m P2 *m C *m block_mx Q2 0 0 1%:M =
lift0_mx L1 *m block_mx d2`_0%:M r 0 H'.
lift0_mx L1 *m block_mx (d2`_0)%:M r 0 H'.
rewrite -!mulmxA; congr (_ *m _); rewrite mulmxA [C]surgery2 -mulmxA.
rewrite (mul_row_block D) ?simplmx mul_mx_row mulmxA -/H -[H]submxK.
f_equal; apply/rowP=> i; rewrite !mxE H1 ?ord1 ?lshift0;
by case: splitP=> // j hj; rewrite !mxE -hj.
rewrite -[lift0_mx L1 *m _ *m _]mulmxA (mulmx_block d2`_0%:M r) ?simplmx.
rewrite -[lift0_mx L1 *m _ *m _]mulmxA (mulmx_block (d2`_0)%:M r) ?simplmx.
rewrite mulmx_block ?simplmx mulmxA -mulmxDl mulmxN mul_scalar_mx.
have -> : - (d2`_0 *: r') + r = 0.
apply/rowP=> i; rewrite 4!mxE.
Expand Down
6 changes: 3 additions & 3 deletions theory/similar.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
(** This file is part of CoqEAL, the Coq Effective Algebra Library.
(c) Copyright INRIA and University of Gothenburg, see LICENSE *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype fintype finfun ssrnat seq.
From mathcomp Require Import choice ssralg poly polydiv mxpoly matrix bigop.
From mathcomp Require Import mxalgebra perm fingroup tuple.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice ssrnat seq.
From mathcomp Require Import bigop fintype finfun ssralg poly polydiv matrix.
From mathcomp Require Import mxalgebra mxpoly perm fingroup tuple.
Require Import mxstructure dvdring.

(** This file contains the definitions of similarity and equivalence
Expand Down
Loading