Helper

submx_castmx

File dumas2017dual/lib/rouche_capelli.v
Section FiniteSolutionCounting
Type Lemma
Proof Lines 7

Signature

Lemma submx_castmx m1 m2 n (A : 'M[K]_(m1, n)) (B : 'M[K]_(m2, n)) e : (A <= B)%MS -> @submx.body K m1 m2 n A (castmx e B).

Description

Submatrix relation preserved under dimension cast: A ≤ B implies A ≤ cast(B). Technical lemma for handling dimension changes in matrix row spaces.

Uses (0)

This lemma does not use any other lemmas from the stats.

Used By (0)

No lemmas in the stats use this lemma.

Coq Source Code

View on GitHub 
Loading source code...
← Back to Stats