Matrix.UnitaryGroup.toLin'_mul
theorem Matrix.UnitaryGroup.toLin'_mul :
∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
(A B : ↥(Matrix.unitaryGroup n α)),
Matrix.UnitaryGroup.toLin' (A * B) = Matrix.UnitaryGroup.toLin' A ∘ₗ Matrix.UnitaryGroup.toLin' B
The theorem `Matrix.UnitaryGroup.toLin'_mul` states that for any type `n` with decidable equality and finiteness, and any type `α` with a commutative ring and star ring structure, given two elements `A` and `B` of the unitary group of `n x n` matrices with entries from `α`, the linear map corresponding to the product of `A` and `B` is equal to the composition of the linear maps corresponding to `A` and `B`. In other words, this theorem shows that matrix multiplication corresponds to composition of linear maps in the context of unitary group.
More concisely: For any commutative ring and star ring `α` with decidable equality and finiteness, and for any `n x n` unitary matrices `A` and `B` over `α`, the product of `A` and `B` as matrices equals the composition of the linear transformations represented by `A` and `B`.
|
Matrix.UnitaryGroup.toLin'_one
theorem Matrix.UnitaryGroup.toLin'_one :
∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α],
Matrix.UnitaryGroup.toLin' 1 = LinearMap.id
The theorem `Matrix.UnitaryGroup.toLin'_one` states that for any type `n` with decidable equality and finiteness, and for any commutative ring with a star operation `α`, the linear map corresponding to the matrix multiplication by the identity element of the unitary group (as defined by `Matrix.UnitaryGroup.toLin' 1`) is the same as the identity linear map (`LinearMap.id`). In other words, this theorem guarantees that applying the matrix multiplication by the identity matrix to vectors is equivalent to performing the identity operation on those vectors, preserving their values.
More concisely: The theorem asserts that the linear map represented by the identity matrix in the unitary group of a commutative ring with a star operation, as defined in Lean, is equal to the identity linear map.
|