Matrix.GeneralLinearGroup.ext
theorem Matrix.GeneralLinearGroup.ext :
∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] ⦃A B : GL n R⦄,
(∀ (i j : n), ↑A i j = ↑B i j) → A = B
The theorem `Matrix.GeneralLinearGroup.ext` asserts that for a given type `n`, where `n` has decidable equality and is a finite type, and for any commutative ring `R`, if two general linear group matrices `A` and `B` of type `GL n R` have all corresponding entries equal (i.e., for all `i` and `j` in `n`, the entries of `A` and `B` at position `(i, j)` are equal), then the two matrices `A` and `B` themselves are equal.
More concisely: For any finite type `n` with decidable equality and commutative ring `R`, if all entries of `GL n R` matrices `A` and `B` are equal, then matrices `A` and `B` are equal.
|
Matrix.SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix
theorem Matrix.SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix :
∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : LinearOrderedCommRing R]
(g : Matrix.SpecialLinearGroup n R), ↑↑(Matrix.SpecialLinearGroup.toGLPos g) = ↑g
This theorem states that for any special linear group `g` (which is a group of `n` by `n` matrices with entries in a linearly ordered commutative ring `R`, and determinant equal to 1), the process of first coercing `g` to a group of invertible matrices with positive determinant (`GL_pos`), and then further coercing to a regular matrix (`GL`), is equivalent to directly coercing `g` to a regular matrix. This theorem is true for any `n` and `R` where `n` is a type with decidable equality and finite number of elements, and `R` is a type with the structure of a linearly ordered commutative ring.
More concisely: For any special linear group `g` of `n` by `n` invertible matrices over a linearly ordered commutative ring `R` with determinant equal to 1, the coercions from `g` to the group of invertible matrices with positive determinant and then to the group of regular matrices are equal.
|