이사벨 : A * 1과 A ** 매트 1의 차이점

Question

에 대해서 *과 **의 차이점은 무엇이며 A * 1 and A ** mat 1`은 무엇입니까?

예 :

가 이사벨에

lemma myexample: 
    fixes A :: "('a::comm_ring_1)^'n∷finite^'n∷finite" 
    shows "(A * 1 = A) ∧ (A ** (mat 1) = A)" 
by (metis comm_semiring_1_class.normalizing_semiring_rules(12) matrix_mul_rid) 

Answer 1

행렬 단순히 벡터의 벡터로 정의되므로, 매트릭스에 * 벡터들로부터 계승되어, 벡터에 * 단지 componentwise 승산이다. 따라서 (A*B) $ i $ j = A $ i $ j * B $ i $ j입니다. 즉, *은 행렬의 항목 별 곱셈입니다. 이것이 실제로 어디서나 유용할지 여부는 모르겠습니다. 나는 그렇게 생각하지 않습니다. 아마 벡터의 벡터로 행렬을 정의하는 아티팩트 일 겁니다. 행렬에 대한 적절한 typedef를 작성하고 행렬 곱셈을 사용하여 행렬 곱셈을 정의하는 것이 더 좋았을 수 있습니다. 그러나 더 많은 작업과 많은 양의 코드가 필요했기 때문에 그 이유가 있었어야합니다. .

**은 적절한 행렬 곱셈입니다. mat x은 대각선에 x이 있고 그 밖의 모든 부분에 0이있는 매트릭스이므로 물론 mat 1은 단위 행렬이며 A ** mat 1 = A입니다.

그러나 매트릭스 1은 다시 벡터 정의의 아티팩트입니다. n 차원 벡터 1은 단순히 n 구성 요소를 갖는 벡터로 정의되며, 모두는 1입니다. 결과적으로 행렬 1은 항목이 모두 1이고, 물론 인 행렬입니다. 이것은 어떤 식 으로든 나에게 유용하지 않은 것 같습니다.