視頻鏈接，求個贊哦：

陶哲軒必備助手之人工智能數學驗證+定理發(fā)明工具LEAN4 [線性代數篇2]矩陣乘積的行列式變形（下篇）_嗶哩嗶哩_bilibili

import Mathlib.LinearAlgebra.Matrix.Determinant

import Mathlib.GroupTheory.Perm.Fin

import Mathlib.GroupTheory.Perm.Sign

import Mathlib.Data.Real.Sqrt

import Mathlib.Data.List.Perm

-- 本文件最終目標是證明行列式中矩陣相乘的運算規(guī)律：第二篇

-- det (M * N) = det M * det N

universe u v w z

open Equiv Equiv.Perm Finset Function

namespace Matrix --目的是避免模糊定義mul_apply

open Matrix BigOperators

variable {m n : Type*} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m]

variable {R : Type v} [CommRing R]

local notation "ε " σ:arg => ((sign σ : ?) : R) -- “元編程”，創(chuàng)造新符號，ε 接收一個參數，結果就是sign σ

set_option linter.unusedVariables false --

-- 沒講到的部分會分別用“前置知識”視頻發(fā)出來，先記???

?

def detRowAlternating2

: AlternatingMap R (n → R) R n --- 最后這個參數n屬于補充說明,實際形式上只需傳三個參數即可

:=

MultilinearMap.alternatization ( -- ???基本的要素都齊了，求和，連乘，全體置換，置換的符號。具體邏輯還不懂

(MultilinearMap.mkPiAlgebra R n R).compLinearMap

LinearMap.proj)

abbrev det2 (M : Matrix n n R): R :=

(detRowAlternating2) M -- 這里為什么類型是R，因為detRowAlternating2相當于detRowAlternating2.toFun

?

-- 前置知識

-- Perm 的使用,排列組合

-- 以下是一些關于 Perm n 的示例，其中 n 取不同的值：

-- 當 n = 1 時，Perm 1 表示長度為 1 的置換，即 [0]。

-- 當 n = 2 時，Perm 2 表示長度為 2 的置換，共有兩種情況：[0, 1] 和 [1, 0]。

-- 當 n = 3 時，Perm 3 表示長度為 3 的置換，共有六種情況：[0, 1, 2]、[0, 2, 1]、[1, 0, 2]、[1, 2, 0]、[2, 0, 1] 和 [2, 1, 0]。

-- #eval Finset.val (Finset.univ : Finset (Fin 4))

def printPerms (n : ?) : List (List ?) :=

List.map List.reverse (List.permutations (List.range n))

-- ???Perm n的理解錯了：Perm n即Equiv α α

-- α ? α 則是 Equiv α α的記號

-- α ? β is the type of functions from α → β with a two-sided inverse，是有雙邊逆的映射，而不是等價關系。

-- #check Perm n

-- #eval printPerms 4

-- #eval printPerms 3 -- [0, 1, 2] [2, 1, 0]

?

-- 正式開始：

lemma MainGoal_1 (M N : Matrix n n R) :

det (M * N)

= ∑ p : n → n, -- {1,2,3} → {1,2,3}

∑ σ : Perm n,

ε σ

*

∏ i,

M (σ i) (p i) * N (p i) i

:= by

simp only [det_apply']

simp only [mul_apply]

simp only [prod_univ_sum] -- ???與"先連加，再連乘，等于，先連乘，再連加"，還有笛卡爾積“全覆蓋”，相關的定理

-- 如何理解Fintype.piFinset t

-- 假設 t 是一個從集合 {1, 2} 到有限集合的映射，其中 t(1) = {a, b}，t(2) = {x, y}。

-- 那么 Fintype.piFinset t 就表示集合 {(a, x), (a, y), (b, x), (b, y)}，即這兩個集合的笛卡爾積。

-- 舉例說明prod_univ_sum

-- 首先，讓我們假設集合α包含元素1和2，對應的集合分別為t1和t2。而且我們有以下映射關系：

-- t1 = {a, b}, t2 = {x, y}

-- 對應的函數f如下：

-- f(1, a) = 2, f(1, b) = 3, f(2, x) = 1, f(2, y) = 4

-- 現在我們來計算左側和右側的值。

-- 左側：(∏ a, ∑ b in t a, f a b)

-- = (∑ b in t1, f(1, b)) * (∑ b in t2, f(2, b))

-- = (f(1, a) + f(1, b)) * (f(2, x) + f(2, y))

-- = (2 + 3) * (1 + 4)

-- = 5 * 5

-- = 25

-- 右側：∑ p in Fintype.piFinset t, ∏ x, f x (p x)

-- = f(1, a) * f(2, x) + f(1, a) * f(2, y) + f(1, b) * f(2, x) + f(1, b) * f(2, y)

-- = 2 * 1 + 2 * 4 + 3 * 1 + 3 * 4

-- = 2 + 8 + 3 + 12

-- = 25

-- 因此，根據 Finset.prod_univ_sum 定理，左側和右側的值相等，都等于25。

simp only [mul_sum]

simp only [Fintype.piFinset_univ]--???

rw [Finset.sum_comm]

done

?

lemma MainGoal_2 (M N : Matrix n n R):

∑ p : n → n,

∑ σ : Perm n,

(ε σ)

*

∏ i,

M (σ i) (p i) * N (p i) i

= ∑ p in (@univ (n → n) _).filter Bijective,

∑ σ : Perm n,

ε σ

*

(∏ i,

M (σ i) (p i) * N (p i) i)

:= by

apply Eq.symm

apply sum_subset --s? ? s?， x ∈ s?, x ? s?的情況為0，則可以直接去掉

· intro h1 h2

exact mem_univ h1

· intros h3 h4 h5

apply det_mul_aux -- ???這個先不理解，后面專門出一個視頻來教如何讀證明并且分解證明成策略模式。

-- 一個先連乘，再連加的東西，結果是0，關鍵是非雙射導致的，有點意思

-- 舉個例子，p=[1,1],Perm 2只有兩個變換：1.恒等變換，簡稱id；2.換位變換，簡稱swap

-- ε id * (M (id 1)(p 1) * N (p 1)1) * (M (id 2)(p 2) * N (p 2)2)

-- = 1 * (M 1 1 * N 1 1) * (M 2 1 * N 1 2)

-- = M 1 1 * N 1 1 * M 2 1 * N 1 2

-- ε swap * (M (swap 1)(p 1) * N (p 1)1) * (M (swap 2)(p 2) * N (p 2)2)

-- = -1 * (M 2 1 * N 1 2) * (M 1 1 * N 1 1)

-- = -M 2 1 * N 1 2 * M 1 1 * N 1 1

simp only [mem_filter] at h5 -- 就是filter的定義唄，是屬于某個集合里面的，而且滿足條件1

simp only [mem_univ] at h5

simp only [true_and_iff] at h5

set h6 := fun x ? h3 x -- 寫這個h6,h7是為了補充說明，其實這里h6就是和h3同一個映射，寫法不一樣而已

-- have h7: h6=h3 --為了講解而寫的

-- := by

-- exact rfl

exact h5

done

?

lemma MainGoal_3 (M N : Matrix n n R):

∑ p in (@univ (n → n) _).filter Bijective,

∑ σ: Perm n,

ε σ

*

(∏ i,

M (σ i) (p i) * N (p i) i)

=

∑ τ : Perm n,

∑ σ : Perm n,

(ε σ)

*

(∏ i,

M (σ i) (τ i) * N (τ i) i)

:= by

rw [sum_comm]

rw [sum_comm] -- 這兩步sum_comm相當于沒變，只改成了x,y

-- 反向推理

refine' sum_bij _ _ _ _ _ -- ???這個需要問一下gpt找到數學世界里的對應定理名稱。不一樣的定義域s、t，不同的函數f、g，求和相同，需要什么條件呢。5個條件

-- 舉例：

-- 假設我們有以下集合和映射：

-- 令 α = {1, 2, 3}，即集合 {1, 2, 3}。

-- 令 β = {a, b, c}，即集合 {a, b, c}。

-- 令 γ = {x, y, z}，即集合 {x, y, z}。

-- 定義函數 f: α → β 和 g: γ → β 如下：

-- 對于 f，我們定義 f(1) = a，f(2) = b，f(3) = c。

-- 對于 g，我們定義 g(x) = a，g(y) = b，g(z) = c。

-- 接下來，定義函數 i: α → γ 如下：

-- i(1) = x

-- i(2) = y

-- i(3) = z

-- 現在，我們可以檢查定理的條件是否滿足：

-- 映射關系 (h)： 對于所有 a 屬于 {1, 2, 3}，我們有 f a = g (i a)。

-- 這是滿足的，例如，對于 a = 1，我們有 f(1) = a 和 g(i(1)) = g(x) = a。

-- i 是單射 (i_inj)： 如果 i a? = i a?，則 a? = a?。

-- 這是滿足的，因為 i 的定義是一對一的，不同的 a 映射到不同的 γ 中的元素。

-- i 是滿射 (i_surj)： 對于任意 b 屬于 {x, y, z}，存在 a 屬于 {1, 2, 3}，使得 b = i a。

-- 這也是滿足的，因為 i 的定義覆蓋了整個 γ。

-- 如果這些條件滿足，我們可以應用定理，從而得出：

-- [

-- \prod_{x \in {1, 2, 3}} f(x) = \prod_{x \in {x, y, z}} g(x)

-- ]

-- 即，

-- [

-- abc = abc

-- ]

· intros ih1 ih2 -- 這里ih1潛臺詞是隨機的ih1

-- 感性理解就是容易犯錯，不想犯錯還是得程序驗證

simp only [Perm]

have ih3:= (mem_filter.mp ih2).right

have ih4:= ofBijective ih1 ih3 -- 單射+滿射的映射，向上升級概念為（或者叫自然拓展性質）：具有雙邊逆的映射（實質并沒有發(fā)生任何變化）

-- 提一句：通常名字為of的函數，就是講一些等價的概念互相轉換。

exact ih4 -- 如果這里定義錯了，下面滿盤皆輸

-- 證明的一個哲學意義是：給出某一個例子，是屬于這個命題說的類的。

-- 注意不能像以下這樣定義

-- intros ih1 ih2

-- have ih3:= Equiv.refl n

-- simp only [Perm]

-- exact ih3

· intro h1

intro h2 --原來這里會用到refine1的證明

simp only [mem_univ]

· intros h_1 h_2

have h_3:= mem_filter.1 h_2

obtain ?h_4,h_5? := h_3

simp only [id_eq]

set h_6 := ofBijective h_1 h_5 -- h_1和h_6相等嗎？，由ofBijective的toFun定義知道就是h_1

-- have h1_equal_h6 : h_1=h_6 --為了講解

-- := by

-- exact rfl

rfl

· intros inj_1 inj_2 inj_3 inj_4 inj_5

simp only [id_eq] at inj_5 -- 看起來很明顯，但就是完成不了

ext x

have inj_6:= ofBijective_apply inj_1

have inj_7:= ofBijective_apply inj_2

rw [

← inj_6,

inj_5,

inj_7]

done

· intros b x

refine' Exists.intro b _ -- 存在，給出例子，然后代入第二個參數中，比如這里就是把a全部替換成了b

-- 如果第二個參數中不用直接替換的，比如下面這行，就直接證明第二個參數代表的命題即可

refine' Exists.intro _ _ -- 比如這里ha在第二個參數中沒有需要替換的，直接證明第二個命題即可

· refine' mem_filter.2 _

constructor

· refine' mem_univ (↑b)

· exact Equiv.bijective b

· -- refine' coe_fn_injective _ --在外層套了一個不變的映射

simp only [id_eq]

-- simp only [FunLike.coe_fn_eq]

refine' Equiv.ext _

intros x2

-- ↑(ofBijective ↑b (_ : Bijective ↑b))前面這個和↑b作用效果一樣嗎?查一下ofBijective的toFun := f定義就知道，就是f本身

-- 下面是進一步的探究，不看了

-- have equalTest: (ofBijective ↑b (_ : Bijective ↑b)) = b

-- := by

-- refine ((fun {α β} {e? e?} ? Equiv.coe_inj.mp) rfl).symm

rfl

done

done

?

lemma MainGoal_4 (M N : Matrix n n R):

∑ τ : Perm n,

∑ σ : Perm n,

(ε σ)

*

(∏ i,

M (σ i) (τ i) * N (τ i) i)

= ∑ σ : Perm n,

∑ τ : Perm n,

(∏ i,

N (σ i) i)

*

(ε τ)

* ∏ j, M (τ j) (σ j)

:= by

simp only [mul_comm]

simp only [mul_left_comm]

simp only [prod_mul_distrib] -- 1個連乘變成2個連乘相關的定理

simp only [mul_assoc]

done

-- ///

def hhh3_h4 (M N : Matrix n n R) (h5: Perm n) (h1: Perm n)

: --映射間組合的一個定理

∏ j,

M (h5 j) (h1 j) =

∏ j,

M ((h5 * h1?1) j) j -- perm n之間的乘法是什么結果呢？還是perm n

:= by

rw [← (h1?1 : _ ? _).prod_comp] -- 兩個函數的連乘的結果一樣的相關證明（感性理解：置換后反正都要遍歷的對吧，連乘應該都一樣的哦）

simp only [Equiv.Perm.coe_mul]

simp only [apply_inv_self]

simp only [Function.comp_apply]

done

def h6 (h5: Perm n) (h1: Perm n)

: (ε h1) * (ε (h5 * h1?1)) -- [1,2,3] => [3,1,2]

= (ε h5) -- 轉置的符號相關的定理

:=

calc

(ε h1) * ε (h5 * h1?1)

= ε (h5 * h1?1 * h1)

:= by

rw [mul_comm, sign_mul (h5 * h1?1)] --???sign_mul

-- simp only [_root_.map_mul]

simp only [sign_mul]

simp only [map_inv]--???map_inv這個證明可以細講

simp only [Int.units_inv_eq_self] -- 1或-1的倒數還是自己

simp only [Units.val_mul] --明明一看就知道相等的。。。

simp only [Int.cast_mul]

_ = ε h5

:= by

simp only [inv_mul_cancel_right]

lemma MainGoal_5 (M N : Matrix n n R):

∑ σ : Perm n,

∑ τ : Perm n,

(∏ i, N (σ i) i)

*

(ε τ)

*

∏ j, M (τ j) (σ j)

=

∑ σ : Perm n,

∑ τ : Perm n,

(∏ i, N (σ i) i)

*

(ε σ * ε τ)

*

∏ i,

M (τ i) i

:= by

refine' sum_congr _ _ --定義域一樣，定義域內f和g的映射值一樣，則兩個求和結果一樣

· rfl

· intros h1 h2

refine' Fintype.sum_equiv _ _ _ _ --兩個不同函數求和的結果一樣的相關證明

· exact Equiv.mulRight h1?1 -- 將映射1變成映射2的一個映射，具體作用是右乘，這是一步需要后面依賴的證明，所以不能隨意證明，通常都是第一步這樣

-- [1,2,3] h1=> [3,2,1] h1?1=> [1,2,3]

-- [1,2,3] h10=> [2,3,1] => [2,1,3]

-- h10 * h1?1 (Perm n)

-- (? * h1?1)

· intros h5 --其實infoview里面的 ?1:?2 這樣的寫法，?1就是一個隨機的屬于?2的對象或元素

simp_rw [Equiv.coe_mulRight]

simp_rw [(h6 h5 h1)]

simp only [(hhh3_h4 M N h5 h1)]

done

?

-- //

?

def MainGoal_6_1_1_1 (M: Matrix n n R)

:= (det_apply' M)

def MainGoal_6_1_1_2 (M: Matrix n n R):

∑ x : Perm n, (ε x) * ∏ x_1 : n, M (x x_1) x_1

= ∑ x : Perm n, (∏ x_1 : n, M (x x_1) x_1) * (ε x) -- 這明明就是一個交換律能完成的，偏要congr一下拆開。。。

:= by

refine' sum_congr _ _

· exact (Eq.refl univ)

· intros h212x h212a

have h2_1_2_1

: (ε h212x) * ∏ x_1 : n, M (h212x x_1) x_1 = (ε h212x) * ∏ x_1 : n, M (h212x x_1) x_1

:= by

exact rfl --竟然直接搞定了

have h2_1_2_2 := mul_comm (ε h212x) (∏ x_1 : n, M (h212x x_1) x_1)

have h2_1_2_3 := h2_1_2_1.trans h2_1_2_2

exact h2_1_2_3

def MainGoal_6_1_1 (M N : Matrix n n R):

det M = ∑ x : Perm n, (∏ x_1 : n, M (x x_1) x_1) * (ε x)

:= by

exact (MainGoal_6_1_1_1 M).trans (MainGoal_6_1_1_2 M) -- .trans就是等號傳遞

def h2_2_1(N : Matrix n n R):= det_apply' N

def h2_2_2(N : Matrix n n R): ∑ x : Perm n, (ε x) * ∏ x_1 : n, N (x x_1) x_1

= ∑ x : Perm n, (∏ x_1 : n, N (x x_1) x_1) * (ε x) -- 又是一個內部交換就好了

:= by

refine' sum_congr _ _

· exact Eq.refl univ

· intros h222x h222a

have h2_2_2_1 : (ε h222x) * ∏ x_1 : n, N (h222x x_1) x_1 = (ε h222x) * ∏ x_1 : n, N (h222x x_1) x_1

:= by

rfl

have h2_2_2_2:= (mul_comm ((ε h222x)) (∏ x_1 : n, N (h222x x_1) x_1))

have h2_2_2_3:= h2_2_2_1.trans h2_2_2_2

exact h2_2_2_3

def MainGoal_6_1_2 (N : Matrix n n R): det N = ∑ x : Perm n, (∏ x_1 : n, N (x x_1) x_1) * (ε x)

:= by

exact (h2_2_1 N).trans (h2_2_2 N)

lemma MainGoal_6_1 (M N : Matrix n n R):

det M * det N

= ∑ x : Perm n,

(∑ x : Perm n, (∏ x_1 : n, M (x x_1) x_1) * (ε x))

*

((∏ x_1 : n, N (x x_1) x_1) * (ε x))

:= by

have temp1:= (MainGoal_6_1_1 M N)

have temp2:= (MainGoal_6_1_2 N)

have h1 := congr (congrArg HMul.hMul temp1) (temp2) -- congr就是相同函數，相同參數，結果一樣的意思；congrArg也是類似的意思

rw [h1]

exact mul_sum

-- exact h1.trans mul_sum

--//

def h3_3 (M N : Matrix n n R) (h3_1: Perm n) (h3_2: h3_1 ∈ univ)

: (∑ x : Perm n,

(∏ x_1 : n, M (x x_1) x_1)

*

(ε x)

)

*

(

(∏ x_1 : n, N (h3_1 x_1) x_1)

*

(ε h3_1)

)

= ∑ x : Perm n,

(∏ x_1 : n, N (h3_1 x_1) x_1)

*

(ε h3_1)

*

(

(∏ x_1 : n, M (x x_1) x_1)

*

(ε x)

)

:= by

have h3_3_1 :

(∑ x : Perm n,

(∏ x_1 : n, M (x x_1) x_1)

*

(ε x)

)

*

(

(∏ x_1 : n, N (h3_1 x_1) x_1)

*

(ε h3_1)

)

=

(∏ x_1 : n, N (h3_1 x_1) x_1)

*

(ε h3_1)

*

∑ x : Perm n,

(∏ x_1 : n, M (x x_1) x_1)

*

(ε x)

:= by

have h3_3_1_1 := mul_comm

(∑ x : Perm n, (∏ x_1 : n, M (x x_1) x_1) * (ε x))

((∏ x_1 : n, N (h3_1 x_1) x_1) * (ε h3_1))

exact h3_3_1_1

have h3_3_2:= h3_3_1.trans mul_sum

exact h3_3_2

def h3_4 (M N : Matrix n n R) (h3_1: Perm n) (h3_2: h3_1 ∈ univ)

:

∑ x_1 : Perm n,

(∏ x_2 : n, N (h3_1 x_2) x_2)

*

(ε h3_1)

*

(

(∏ x : n, M (x_1 x) x)

*

(ε x_1)

)

=

∑ x_1 : Perm n,

(∏ x_2 : n, N (h3_1 x_2) x_2)

*

(

(∏ x : n, M (x_1 x) x)

*

((ε h3_1) * (ε x_1))

) -- 又是交換就可以了。。。

:= by

refine' sum_congr _ _

· exact (Eq.refl univ)

· intros h34x_1 h34a

have h3_4_1 : (∏ x_2 : n, N (h3_1 x_2) x_2) * (ε h3_1) * ((∏ x : n, M (h34x_1 x) x) * (ε h34x_1))

= (∏ x : n, M (h34x_1 x) x) * ((∏ x_2 : n, N (h3_1 x_2) x_2) * ((ε h3_1) * (ε h34x_1)))

:= ((mul_left_comm ((∏ x_2 : n, N (h3_1 x_2) x_2) * (ε h3_1)) (∏ x : n, M (h34x_1 x) x)

(ε h34x_1)).trans

(congrArg (HMul.hMul (∏ x : n, M (h34x_1 x) x))

(mul_assoc (∏ x_2 : n, N (h3_1 x_2) x_2) (ε h3_1) (ε h34x_1))))

have h3_4_2 : (∏ x : n, M (h34x_1 x) x) * ((∏ x_2 : n, N (h3_1 x_2) x_2) * ((ε h3_1) * (ε h34x_1)))

=(∏ x_2 : n, N (h3_1 x_2) x_2) * ((∏ x : n, M (h34x_1 x) x) * ((ε h3_1) * (ε h34x_1)))

:= (mul_left_comm (∏ x : n, M (h34x_1 x) x) (∏ x_2 : n, N (h3_1 x_2) x_2)

((ε h3_1) * (ε h34x_1)))

have h3_4_3:= h3_4_1.trans h3_4_2

exact h3_4_3

lemma MainGoal_6_2 (M N : Matrix n n R)

:

∑ x : Perm n,

(∑ x : Perm n,

(∏ x_1 : n, M (x x_1) x_1)

*

(ε x)

)

*

(

(∏ x_1 : n, N (x x_1) x_1)

*

(ε x)

)

=

∑ x : Perm n,

∑ x_1 : Perm n,

(∏ x_2 : n, N (x x_2) x_2)

*

(

(∏ x : n,M (x_1 x) x)

*

((ε x) * (ε x_1))

)

:= by

have h2 := MainGoal_6_1 M N

refine' sum_congr _ _

· exact (Eq.refl univ)

· intros h3_1 h3_2

have h3_5:= (h3_3 M N h3_1 h3_2).trans (h3_4 M N h3_1 h3_2)

exact h3_5

--//

def MainGoal_6_3 (M N : Matrix n n R):= (MainGoal_6_1 M N).trans (MainGoal_6_2 M N)

lemma MainGoal_6 (M N : Matrix n n R):

∑ σ : Perm n,

∑ τ : Perm n,

(∏ i, N (σ i) i)

*

(ε σ * ε τ)

*

(∏ i, M (τ i) i)

= det M * det N

:= by

have h4:= MainGoal_6_3 M N

simp only [h4]

congr -- 去掉兩邊套在最外的，恰好是相同的函數

funext xx1

congr

funext xx2

rw [mul_right_comm]

repeat rw [← mul_assoc]

done

?

-- @[simp]

theorem MainGoal (M N : Matrix n n R)

: det (M * N) = det M * det N

:= by

have h1 :det (M * N) = det M * det N :=

calc

det (M * N)

= ∑ p : n → n, ∑ σ : Perm n, ε σ * ∏ i, M (σ i) (p i) * N (p i) i --第1個變式

:= by

exact MainGoal_1 M N

_ = ∑ p in (@univ (n → n) _).filter Bijective,--第2個變式

∑ σ : Perm n,

ε σ

*

(∏ i, M (σ i) (p i) * N (p i) i)

:= by

exact MainGoal_2 M N

_ = ∑ τ : Perm n, --第3個變式

∑ σ : Perm n,

(ε σ)

*

(∏ i,

M (σ i) (τ i) * N (τ i) i)

:= by

exact MainGoal_3 M N

_ = ∑ σ : Perm n,--第4個變式

∑ τ : Perm n,

(∏ i, N (σ i) i)

*

ε τ

*

∏ j, M (τ j) (σ j)

:= by

exact MainGoal_4 M N

_ = ∑ σ : Perm n, --第5個變式

∑ τ : Perm n,

(∏ i, N (σ i) i)

*

(ε σ * ε τ)

*

∏ i,

M (τ i) i

:= by

exact MainGoal_5 M N

_ = det M * det N --第6個變式

:= by

-- simp only [det_apply', Finset.mul_sum, mul_comm, mul_left_comm, mul_assoc] --這里無法分步，所以直接分析print來寫成下面這樣子：

exact MainGoal_6 M N

exact h1

done

?

end Matrix文章來源地址http://www.zghlxwxcb.cn/news/detail-816692.html

到了這里，關于陶哲軒必備助手之人工智能數學驗證+定理發(fā)明工具LEAN4 [線性代數篇2]矩陣乘積的行列式變形（下篇）的文章就介紹完了。如果您還想了解更多內容，請在右上角搜索TOY模板網以前的文章或繼續(xù)瀏覽下面的相關文章，希望大家以后多多支持TOY模板網！