视频链接，有空点进去点个赞哦，谢谢支持：
陶哲轩工作流之人工智能数学验证+定理发明工具LEAN4 [线性代数篇2前置知识]笛卡尔积等价于映射n → n全体_哔哩哔哩_bilibili
--n是有限的 n → n -- Fintype.piFinset fun a ? univ 笛卡尔积 ， t(1)={1,2}, t(2)={1,2} -- 两者为什么恰好相等？ -- 举例说明n=2 , n={1,2} → n={1,2} -- 对于任意个映射f : n → n -- 1 => ? 1/2 -- 2 => ? 1/2 -- 1 => 2 -- 2 => 1 -- 写成（2，1）， -- （1，1），（1，2）， （2，2） -- 实际上就是n={1,2} 分别映射到→ n={2,1} -- 笛卡尔积是什么呢(1,1) (1,2) (2,1) (2,2) /-----/ -- 再举例说明n=3, t(1)={1,2,3}, t(2)={1,2,3}， t(3)={1,2,3} -- n={1,2,3} → n={1,2,3} -- 对于某个映射f : n → n -- 1 => ? 1/2/3 -- 2 => ? 1/2/3 -- 3 => ? 1/2/3 -- 写成（2，1，3）...... -- 笛卡尔积是什么呢（1，3，2），（2，1，3）