ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>n : ℕ<VAR>s : Affine.Simplex k P n<VAR>fs : Finset (Fin (n + 1))<VAR>m : ℕ<VAR>h : fs.card = m + 1<GOAL>(s.face h).points = s.points ∘ ⇑(fs.orderEmbOfFin h)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>n : ℕ<VAR>s : Affine.Simplex k P n<VAR>i : Fin (n + 1)<GOAL>s.face ⋯ = Affine.Simplex.mkOfPoint k (s.points i)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>n : ℕ<VAR>s : Affine.Simplex k P n<VAR>fs : Finset (Fin (n + 1))<VAR>m : ℕ<VAR>h : fs.card = m + 1<GOAL>Set.range (s.face h).points = s.points '' ↑fs
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>m n : ℕ<VAR>s : Affine.Simplex k P m<VAR>e : Fin (m + 1) ≃ Fin (n + 1)<GOAL>∀ (a : Fin (n + 1)), (s.reindex e).points a = (s.points ∘ ⇑e.symm) a
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>n : ℕ<VAR>s : Affine.Simplex k P n<GOAL>s.reindex (Equiv.refl (Fin (n + 1))) = s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>n₁ n₂ n₃ : ℕ<VAR>e₁₂ : Fin (n₁ + 1) ≃ Fin (n₂ + 1)<VAR>e₂₃ : Fin (n₂ + 1) ≃ Fin (n₃ + 1)<VAR>s : Affine.Simplex k P n₁<GOAL>s.reindex (e₁₂.trans e₂₃) = (s.reindex e₁₂).reindex e₂₃
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>m n : ℕ<VAR>s : Affine.Simplex k P m<VAR>e : Fin (m + 1) ≃ Fin (n + 1)<GOAL>(s.reindex e).reindex e.symm = s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>m n : ℕ<VAR>s : Affine.Simplex k P m<VAR>e : Fin (n + 1) ≃ Fin (m + 1)<GOAL>(s.reindex e.symm).reindex e = s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>m n : ℕ<VAR>s : Affine.Simplex k P m<VAR>e : Fin (m + 1) ≃ Fin (n + 1)<GOAL>Set.range (s.reindex e).points = Set.range s.points
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>n : ℕ<VAR>s : Affine.Simplex k P n<VAR>fs : Finset (Fin (n + 1))<VAR>m : ℕ<VAR>h : fs.card = m + 1<GOAL>Finset.centroid k Finset.univ (s.face h).points = Finset.centroid k fs s.points
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>CharZero k<VAR>n : ℕ<VAR>s : Affine.Simplex k P n<VAR>fs₁ fs₂ : Finset (Fin (n + 1))<VAR>m₁ m₂ : ℕ<VAR>h₁ : fs₁.card = m₁ + 1<VAR>h₂ : fs₂.card = m₂ + 1<GOAL>Finset.centroid k fs₁ s.points = Finset.centroid k fs₂ s.points ↔ fs₁ = fs₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>CharZero k<VAR>n : ℕ<VAR>s : Affine.Simplex k P n<VAR>fs₁ fs₂ : Finset (Fin (n + 1))<VAR>m₁ m₂ : ℕ<VAR>h₁ : fs₁.card = m₁ + 1<VAR>h₂ : fs₂.card = m₂ + 1<GOAL>Finset.centroid k Finset.univ (s.face h₁).points = Finset.centroid k Finset.univ (s.face h₂).points ↔ fs₁ = fs₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>n : ℕ<VAR>s₁ s₂ : Affine.Simplex k P n<VAR>h : Set.range s₁.points = Set.range s₂.points<GOAL>Finset.centroid k Finset.univ s₁.points = Finset.centroid k Finset.univ s₂.points
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>DecidableEq ι<VAR>A : Matrix ι ι R<VAR>w : ι → R<GOAL>((PiToModule.fromMatrix R b) A) w = ((Fintype.total R R) b) (A *ᵥ w)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>DecidableEq ι<VAR>A : Matrix ι ι R<VAR>j : ι<GOAL>((PiToModule.fromMatrix R b) A) (Pi.single j 1) = ∑ i : ι, A i j • b i
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>f : Module.End R M<VAR>w : ι → R<GOAL>((PiToModule.fromEnd R b) f) w = f (((Fintype.total R R) b) w)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>DecidableEq ι<VAR>f : Module.End R M<VAR>i : ι<GOAL>((PiToModule.fromEnd R b) f) (Pi.single i 1) = f (b i)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<GOAL>Function.Injective ⇑(PiToModule.fromEnd R b)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>DecidableEq ι<VAR>A : Matrix ι ι R<VAR>f : Module.End R M<VAR>h : Matrix.Represents b A f<VAR>x : ι → R<GOAL>((Fintype.total R R) b) (A *ᵥ x) = f (((Fintype.total R R) b) x)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>DecidableEq ι<VAR>A : Matrix ι ι R<VAR>f : Module.End R M<GOAL>Matrix.Represents b A f ↔ ∀ (x : ι → R), ((Fintype.total R R) b) (A *ᵥ x) = f (((Fintype.total R R) b) x)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>DecidableEq ι<VAR>A : Matrix ι ι R<VAR>f : Module.End R M<GOAL>Matrix.Represents b A f ↔ ∀ (j : ι), ∑ i : ι, A i j • b i = f (b j)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>DecidableEq ι<VAR>A A' : Matrix ι ι R<VAR>f f' : Module.End R M<VAR>h : Matrix.Represents b A f<VAR>h' : Matrix.Represents b A' f'<GOAL>Matrix.Represents b (A * A') (f * f')
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>DecidableEq ι<GOAL>Matrix.Represents b 1 1
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>DecidableEq ι<VAR>A A' : Matrix ι ι R<VAR>f f' : Module.End R M<VAR>h : Matrix.Represents b A f<VAR>h' : Matrix.Represents b A' f'<GOAL>Matrix.Represents b (A + A') (f + f')
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>DecidableEq ι<GOAL>Matrix.Represents b 0 0
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>DecidableEq ι<VAR>A : Matrix ι ι R<VAR>f : Module.End R M<VAR>h : Matrix.Represents b A f<VAR>r : R<GOAL>Matrix.Represents b (r • A) (r • f)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>DecidableEq ι<VAR>r : R<GOAL>Matrix.Represents b ((algebraMap R (Matrix ι ι R)) r) ((algebraMap R (Module.End R M)) r)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>DecidableEq ι<VAR>A : Matrix ι ι R<VAR>f f' : Module.End R M<VAR>h : Matrix.Represents b A f<VAR>h' : Matrix.Represents b A f'<GOAL>f = f'
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>DecidableEq ι<VAR>A : ↥(Matrix.isRepresentation R b)<GOAL>Matrix.Represents b (↑A) ((Matrix.isRepresentation.toEnd R b hb) A)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>DecidableEq ι<VAR>A : ↥(Matrix.isRepresentation R b)<VAR>f : Module.End R M<VAR>h : Matrix.Represents b (↑A) f<GOAL>(Matrix.isRepresentation.toEnd R b hb) A = f
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>DecidableEq ι<VAR>f : Module.End R M<VAR>I : Ideal R<VAR>hI : LinearMap.range f ≤ I • ⊤<GOAL>∃ M_1, (Matrix.isRepresentation.toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>DecidableEq ι<GOAL>Function.Surjective ⇑(Matrix.isRepresentation.toEnd R b hb)
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>Module.Finite R M<VAR>f : Module.End R M<VAR>I : Ideal R<VAR>hI : LinearMap.range f ≤ I • ⊤<GOAL>∃ p, p.Monic ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (Polynomial.aeval f) p = 0
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>Module.Finite R M<VAR>f : Module.End R M<GOAL>∃ p, p.Monic ∧ (Polynomial.aeval f) p = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>m' : Type u_6<VAR>n' : Type u_7<VAR>R : Type u_11<VAR>A : Type u_12<VAR>Semiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>eₘ : m ≃ m'<VAR>eₙ : n ≃ n'<VAR>M : Matrix m n A<GOAL>(Matrix.reindexLinearEquiv R A eₘ eₙ) M = (Matrix.reindex eₘ eₙ) M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>m' : Type u_6<VAR>n' : Type u_7<VAR>R : Type u_11<VAR>A : Type u_12<VAR>Semiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>eₘ : m ≃ m'<VAR>eₙ : n ≃ n'<GOAL>(Matrix.reindexLinearEquiv R A eₘ eₙ).symm = Matrix.reindexLinearEquiv R A eₘ.symm eₙ.symm
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_11<VAR>A : Type u_12<VAR>Semiring R<VAR>AddCommMonoid A<VAR>Module R A<GOAL>Matrix.reindexLinearEquiv R A (Equiv.refl m) (Equiv.refl n) = LinearEquiv.refl R (Matrix m n A)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>m' : Type u_6<VAR>n' : Type u_7<VAR>m'' : Type u_9<VAR>n'' : Type u_10<VAR>R : Type u_11<VAR>A : Type u_12<VAR>Semiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>e₁ : m ≃ m'<VAR>e₂ : n ≃ n'<VAR>e₁' : m' ≃ m''<VAR>e₂' : n' ≃ n''<GOAL>Matrix.reindexLinearEquiv R A e₁ e₂ ≪≫ₗ Matrix.reindexLinearEquiv R A e₁' e₂' = Matrix.reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>m' : Type u_6<VAR>n' : Type u_7<VAR>m'' : Type u_9<VAR>n'' : Type u_10<VAR>R : Type u_11<VAR>A : Type u_12<VAR>Semiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>e₁ : m ≃ m'<VAR>e₂ : n ≃ n'<VAR>e₁' : m' ≃ m''<VAR>e₂' : n' ≃ n''<GOAL>⇑(Matrix.reindexLinearEquiv R A e₁' e₂') ∘ ⇑(Matrix.reindexLinearEquiv R A e₁ e₂) = ⇑(Matrix.reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂'))
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>m' : Type u_6<VAR>n' : Type u_7<VAR>m'' : Type u_9<VAR>n'' : Type u_10<VAR>R : Type u_11<VAR>A : Type u_12<VAR>Semiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>e₁ : m ≃ m'<VAR>e₂ : n ≃ n'<VAR>e₁' : m' ≃ m''<VAR>e₂' : n' ≃ n''<VAR>M : Matrix m n A<GOAL>(Matrix.reindexLinearEquiv R A e₁' e₂') ((Matrix.reindexLinearEquiv R A e₁ e₂) M) = (Matrix.reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')) M
<VAR>m : Type u_2<VAR>m' : Type u_6<VAR>R : Type u_11<VAR>A : Type u_12<VAR>Semiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>DecidableEq m<VAR>DecidableEq m'<VAR>One A<VAR>e : m ≃ m'<GOAL>(Matrix.reindexLinearEquiv R A e e) 1 = 1
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : Type u_6<VAR>n' : Type u_7<VAR>o' : Type u_8<VAR>R : Type u_11<VAR>A : Type u_12<VAR>Semiring R<VAR>Semiring A<VAR>Module R A<VAR>Fintype n<VAR>Fintype n'<VAR>eₘ : m ≃ m'<VAR>eₙ : n ≃ n'<VAR>eₒ : o ≃ o'<VAR>M : Matrix m n A<VAR>N : Matrix n o A<GOAL>(Matrix.reindexLinearEquiv R A eₘ eₙ) M * (Matrix.reindexLinearEquiv R A eₙ eₒ) N = (Matrix.reindexLinearEquiv R A eₘ eₒ) (M * N)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>n' : Type u_7<VAR>R : Type u_11<VAR>A : Type u_12<VAR>Semiring R<VAR>Semiring A<VAR>Module R A<VAR>Fintype n<VAR>DecidableEq o<VAR>e₁ : o ≃ n<VAR>e₂ : o ≃ n'<VAR>M : Matrix m n A<GOAL>M * (Matrix.reindexLinearEquiv R A e₁ e₂) 1 = (Matrix.reindexLinearEquiv R A (Equiv.refl m) (e₁.symm.trans e₂)) M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_11<VAR>A : Type u_12<VAR>CommSemiring R<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Semiring A<VAR>Algebra R A<VAR>e : m ≃ n<VAR>M : Matrix m m A<GOAL>(Matrix.reindexAlgEquiv R A e) M = (Matrix.reindex e e) M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_11<VAR>A : Type u_12<VAR>CommSemiring R<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Semiring A<VAR>Algebra R A<VAR>e : m ≃ n<GOAL>(Matrix.reindexAlgEquiv R A e).symm = Matrix.reindexAlgEquiv R A e.symm
<VAR>m : Type u_2<VAR>R : Type u_11<VAR>A : Type u_12<VAR>CommSemiring R<VAR>Fintype m<VAR>DecidableEq m<VAR>Semiring A<VAR>Algebra R A<GOAL>Matrix.reindexAlgEquiv R A (Equiv.refl m) = AlgEquiv.refl
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_11<VAR>A : Type u_12<VAR>CommSemiring R<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Semiring A<VAR>Algebra R A<VAR>e : m ≃ n<VAR>M N : Matrix m m A<GOAL>(Matrix.reindexAlgEquiv R A e) (M * N) = (Matrix.reindexAlgEquiv R A e) M * (Matrix.reindexAlgEquiv R A e) N
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_11<VAR>CommRing R<VAR>Fintype m<VAR>DecidableEq m<VAR>Fintype n<VAR>DecidableEq n<VAR>e : m ≃ n<VAR>M : Matrix m m R<GOAL>((Matrix.reindexLinearEquiv R R e e) M).det = M.det
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_11<VAR>B : Type u_13<VAR>CommRing R<VAR>CommRing B<VAR>Algebra R B<VAR>Fintype m<VAR>DecidableEq m<VAR>Fintype n<VAR>DecidableEq n<VAR>e : m ≃ n<VAR>A : Matrix m m B<GOAL>((Matrix.reindexAlgEquiv R B e) A).det = A.det
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A B : Matrix n n α<GOAL>(Polynomial.X • A.map ⇑Polynomial.C + B.map ⇑Polynomial.C).det.natDegree ≤ Fintype.card n
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A B : Matrix n n α<GOAL>(Polynomial.X • A.map ⇑Polynomial.C + B.map ⇑Polynomial.C).det.coeff 0 = B.det
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A B : Matrix n n α<GOAL>(Polynomial.X • A.map ⇑Polynomial.C + B.map ⇑Polynomial.C).det.coeff (Fintype.card n) = A.det
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing α<VAR>A : Matrix n n α<GOAL>(Polynomial.X • 1 + A.map ⇑Polynomial.C).det.leadingCoeff = 1
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>Fintype K<VAR>Fintype V<VAR>k : ℕ<VAR>hk : k ≤ FiniteDimensional.finrank K V<GOAL>Nat.card { s // LinearIndependent K s } = ∏ i : Fin k, (Fintype.card K ^ FiniteDimensional.finrank K V - Fintype.card K ^ ↑i)
<VAR>𝔽 : Type u_1<VAR>Field 𝔽<VAR>Fintype 𝔽<VAR>n : ℕ<GOAL>Nat.card (GL (Fin n) 𝔽) = ∏ i : Fin n, (Fintype.card 𝔽 ^ n - Fintype.card 𝔽 ^ ↑i)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>i : m<VAR>j : n<GOAL>Matrix.mvPolynomialX m n R i j = MvPolynomial.X (i, j)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>A : Matrix m n S<GOAL>(Matrix.mvPolynomialX m n R).map (MvPolynomial.eval₂ f fun p => A p.1 p.2) = A
<VAR>m : Type u_1<VAR>R : Type u_3<VAR>Fintype m<VAR>DecidableEq m<VAR>CommSemiring R<VAR>A : Matrix m m R<GOAL>(MvPolynomial.eval fun p => A p.1 p.2).mapMatrix (Matrix.mvPolynomialX m m R) = A
<VAR>m : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>Fintype m<VAR>DecidableEq m<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>A : Matrix m m S<GOAL>(MvPolynomial.aeval fun p => A p.1 p.2).mapMatrix (Matrix.mvPolynomialX m m R) = A
<VAR>m : Type u_1<VAR>R : Type u_3<VAR>DecidableEq m<VAR>Fintype m<VAR>CommRing R<VAR>Nontrivial R<GOAL>(Matrix.mvPolynomialX m m R).det ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Nontrivial R<VAR>LinearOrderedCommRing S<VAR>n : Type u_3<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n R<VAR>abv : AbsoluteValue R S<VAR>x : S<VAR>hx : ∀ (i j : n), abv (A i j) ≤ x<GOAL>abv A.det ≤ (Fintype.card n).factorial • x ^ Fintype.card n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Nontrivial R<VAR>LinearOrderedCommRing S<VAR>n : Type u_3<VAR>Fintype n<VAR>DecidableEq n<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>A : ι → Matrix n n R<VAR>abv : AbsoluteValue R S<VAR>x : S<VAR>hx : ∀ (k : ι) (i j : n), abv (A k i j) ≤ x<GOAL>abv (∑ k ∈ s, A k).det ≤ (Fintype.card n).factorial • (s.card • x) ^ Fintype.card n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Nontrivial R<VAR>LinearOrderedCommRing S<VAR>n : Type u_3<VAR>Fintype n<VAR>DecidableEq n<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>c : ι → R<VAR>A : ι → Matrix n n R<VAR>abv : AbsoluteValue R S<VAR>x : S<VAR>hx : ∀ (k : ι) (i j : n), abv (A k i j) ≤ x<VAR>y : S<VAR>hy : ∀ (k : ι), abv (c k) ≤ y<GOAL>abv (∑ k ∈ s, c k • A k).det ≤ (Fintype.card n).factorial • (s.card • y * x) ^ Fintype.card n
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>x : M × M₂<GOAL>(LinearMap.fst R M M₂) x = x.1
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>x : M × M₂<GOAL>(LinearMap.snd R M M₂) x = x.2
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>Function.Surjective ⇑(LinearMap.fst R M M₂)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>Function.Surjective ⇑(LinearMap.snd R M M₂)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<VAR>i : M<GOAL>(f.prod g) i = Pi.prod (⇑f) (⇑g) i
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<GOAL>⇑(f.prod g) = Pi.prod ⇑f ⇑g
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<GOAL>LinearMap.fst R M₂ M₃ ∘ₗ f.prod g = f
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<GOAL>LinearMap.snd R M₂ M₃ ∘ₗ f.prod g = g
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>(LinearMap.fst R M M₂).prod (LinearMap.snd R M M₂) = LinearMap.id
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>M₄ : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid M₄<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>f : M₂ →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₄<VAR>h : M →ₗ[R] M₂<GOAL>f.prod g ∘ₗ h = (f ∘ₗ h).prod (g ∘ₗ h)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>S : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module S M₂<VAR>Module S M₃<VAR>SMulCommClass R S M₂<VAR>SMulCommClass R S M₃<VAR>f : (M →ₗ[R] M₂) × (M →ₗ[R] M₃)<GOAL>(LinearMap.prodEquiv S) f = f.1.prod f.2
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>S : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module S M₂<VAR>Module S M₃<VAR>SMulCommClass R S M₂<VAR>SMulCommClass R S M₃<VAR>f : M →ₗ[R] M₂ × M₃<GOAL>(LinearMap.prodEquiv S).symm f = (LinearMap.fst R M₂ M₃ ∘ₗ f, LinearMap.snd R M₂ M₃ ∘ₗ f)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.range (LinearMap.inl R M M₂) = LinearMap.ker (LinearMap.snd R M M₂)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.ker (LinearMap.snd R M M₂) = LinearMap.range (LinearMap.inl R M M₂)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.range (LinearMap.inr R M M₂) = LinearMap.ker (LinearMap.fst R M M₂)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.ker (LinearMap.fst R M M₂) = LinearMap.range (LinearMap.inr R M M₂)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.fst R M M₂ ∘ₗ LinearMap.inl R M M₂ = LinearMap.id
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.snd R M M₂ ∘ₗ LinearMap.inl R M M₂ = 0
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.fst R M M₂ ∘ₗ LinearMap.inr R M M₂ = 0
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.snd R M M₂ ∘ₗ LinearMap.inr R M M₂ = LinearMap.id
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>⇑(LinearMap.inl R M M₂) = fun x => (x, 0)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>x : M<GOAL>(LinearMap.inl R M M₂) x = (x, 0)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>⇑(LinearMap.inr R M M₂) = Prod.mk 0
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>x : M₂<GOAL>(LinearMap.inr R M M₂) x = (0, x)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.inl R M M₂ = LinearMap.id.prod 0
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>LinearMap.inr R M M₂ = LinearMap.prod 0 LinearMap.id
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>Function.Injective ⇑(LinearMap.inl R M M₂)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<GOAL>Function.Injective ⇑(LinearMap.inr R M M₂)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>x : M × M₂<GOAL>(f.coprod g) x = f x.1 + g x.2
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<GOAL>f.coprod g ∘ₗ LinearMap.inl R M M₂ = f
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<GOAL>f.coprod g ∘ₗ LinearMap.inr R M M₂ = g