ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>a : Aᵐᵒᵖ<VAR>b : Bᵐᵒᵖ<GOAL>(Algebra.TensorProduct.opAlgEquiv R S A B) (a ⊗ₜ[R] b) = MulOpposite.op (MulOpposite.unop a ⊗ₜ[R] MulOpposite.unop b)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>a : A<VAR>b : B<GOAL>(Algebra.TensorProduct.opAlgEquiv R S A B).symm (MulOpposite.op (a ⊗ₜ[R] b)) = MulOpposite.op a ⊗ₜ[R] MulOpposite.op b
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>ι : Type u_4<VAR>x : N<VAR>f : ι → R<GOAL>(TensorProduct.piScalarRightHom R S N ι) (x ⊗ₜ[R] f) = fun j => f j • x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>ι : Type u_4<VAR>Fintype ι<VAR>DecidableEq ι<VAR>x : N<VAR>i : ι<GOAL>(TensorProduct.piScalarRightInv R S N ι) (Pi.single i x) = x ⊗ₜ[R] Pi.single i 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>ι : Type u_4<VAR>Fintype ι<VAR>DecidableEq ι<VAR>x : TensorProduct R N (ι → R)<GOAL>(TensorProduct.piScalarRight R S N ι) x = (TensorProduct.piScalarRightHom R S N ι) x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>ι : Type u_4<VAR>Fintype ι<VAR>DecidableEq ι<VAR>x : N<VAR>i : ι<GOAL>(TensorProduct.piScalarRight R S N ι).symm (Pi.single i x) = x ⊗ₜ[R] Pi.single i 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : ι → Type u_4<VAR>f : (ι : ι) → φ ι → M<VAR>hf : ∀ (i : ι), LinearIndependent R (f i)<GOAL>LinearIndependent R fun ix => Finsupp.single ix.fst (f ix.fst ix.snd)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>φ : ι → Type u_4<VAR>b : (i : ι) → Basis (φ i) R M<VAR>g : ι →₀ M<VAR>ix : (i : ι) × φ i<GOAL>((Finsupp.basis b).repr g) ix = ((b ix.fst).repr (g ix.fst)) ix.snd
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>φ : ι → Type u_4<VAR>b : (i : ι) → Basis (φ i) R M<GOAL>⇑(Finsupp.basis b) = fun ix => Finsupp.single ix.fst ((b ix.fst) ix.snd)
<VAR>R : Type u_1<VAR>ι : Type u_3<VAR>Semiring R<GOAL>Finsupp.basisSingleOne.repr = LinearEquiv.refl R (ι →₀ R)
<VAR>R : Type u_1<VAR>ι : Type u_3<VAR>Semiring R<GOAL>⇑Finsupp.basisSingleOne = fun i => Finsupp.single i 1
<VAR>R : Type u_1<VAR>n : Type u_3<VAR>DecidableEq n<VAR>Semiring R<VAR>Fintype n<VAR>a : R<VAR>i : n<GOAL>∑ x : n, Finsupp.single x (if i = x then a else 0) = Finsupp.single i a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>n : Type u_3<VAR>DecidableEq n<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Finite n<VAR>b : Basis n R M<VAR>i : n<GOAL>b.equivFun.symm ((LinearMap.stdBasis R (fun x => R) i) 1) = b i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>Nontrivial R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>ι : Type w<VAR>DecidableEq ι<VAR>Fintype ι<VAR>b : Basis ι R M<GOAL>((LinearMap.toMatrix b b) f).charpoly = f.charpoly
<VAR>R : Type u_1<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>CommRing R<VAR>Nontrivial R<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>Module.Finite R M₁<VAR>Module.Free R M₁<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>Module.Finite R M₂<VAR>Module.Free R M₂<VAR>f₁ : M₁ →ₗ[R] M₁<VAR>f₂ : M₂ →ₗ[R] M₂<GOAL>(f₁.prodMap f₂).charpoly = f₁.charpoly * f₂.charpoly
<VAR>R : Type u_1<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>CommRing R<VAR>Nontrivial R<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>Module.Finite R M₁<VAR>Module.Free R M₁<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>Module.Finite R M₂<VAR>Module.Free R M₂<VAR>e : M₁ ≃ₗ[R] M₂<VAR>φ : Module.End R M₁<GOAL>LinearMap.charpoly (e.conj φ) = LinearMap.charpoly φ
<VAR>A : Type u_5<VAR>CommRing A<VAR>n : Type u_7<VAR>Fintype n<VAR>DecidableEq n<VAR>M N : Matrix n n A<GOAL>(M * N).det = (N * M).det
<VAR>A : Type u_5<VAR>CommRing A<VAR>m : Type u_6<VAR>n : Type u_7<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>M : Matrix n m A<VAR>N M' : Matrix m n A<VAR>hMM' : M * M' = 1<VAR>hM'M : M' * M = 1<GOAL>(M * N).det = (N * M).det
<VAR>A : Type u_5<VAR>CommRing A<VAR>m : Type u_6<VAR>n : Type u_7<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>M : Matrix m n A<VAR>M' : Matrix n m A<VAR>N : Matrix n n A<VAR>hMM' : M * M' = 1<VAR>hM'M : M' * M = 1<GOAL>(M * N * M').det = N.det
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<VAR>κ : Type u_6<VAR>Fintype κ<VAR>DecidableEq κ<VAR>b : Basis ι A M<VAR>c : Basis κ A M<VAR>f : M →ₗ[A] M<GOAL>((LinearMap.toMatrix b b) f).det = ((LinearMap.toMatrix c c) f).det
<VAR>M : Type u_7<VAR>AddCommGroup M<VAR>ι : Type u_8<VAR>DecidableEq ι<VAR>Fintype ι<VAR>A : Type u_9<VAR>CommRing A<VAR>Module A M<GOAL>LinearMap.detAux = Trunc.lift (fun b => Matrix.detMonoidHom.comp ↑(LinearMap.toMatrixAlgEquiv b)) ⋯
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<VAR>b : Basis ι A M<VAR>f : M →ₗ[A] M<GOAL>(LinearMap.detAux (Trunc.mk b)) f = ((LinearMap.toMatrix b b) f).det
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<VAR>ι' : Type u_7<VAR>Fintype ι'<VAR>DecidableEq ι'<VAR>tb : Trunc (Basis ι A M)<VAR>b' : Basis ι' A M<VAR>f : M →ₗ[A] M<GOAL>(LinearMap.detAux tb) f = ((LinearMap.toMatrix b' b') f).det
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<VAR>b : Trunc (Basis ι A M)<GOAL>(LinearMap.detAux b) LinearMap.id = 1
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<VAR>b : Trunc (Basis ι A M)<VAR>f g : M →ₗ[A] M<GOAL>(LinearMap.detAux b) (f ∘ₗ g) = (LinearMap.detAux b) f * (LinearMap.detAux b) g
<VAR>M : Type u_7<VAR>AddCommGroup M<VAR>A : Type u_8<VAR>CommRing A<VAR>Module A M<GOAL>LinearMap.det = if H : ∃ s, Nonempty (Basis { x // x ∈ s } A M) then LinearMap.detAux (Trunc.mk ⋯.some) else 1
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<VAR>DecidableEq M<GOAL>⇑LinearMap.det = ⇑(if H : ∃ s, Nonempty (Basis { x // x ∈ s } A M) then LinearMap.detAux (Trunc.mk ⋯.some) else 1)
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<VAR>DecidableEq M<VAR>s : Finset M<VAR>b : Basis { x // x ∈ s } A M<VAR>f : M →ₗ[A] M<GOAL>LinearMap.det f = ((LinearMap.toMatrix b b) f).det
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<VAR>b : Basis ι A M<VAR>f : M →ₗ[A] M<GOAL>((LinearMap.toMatrix b b) f).det = LinearMap.det f
<VAR>A : Type u_5<VAR>CommRing A<VAR>ι : Type u_7<VAR>Fintype ι<VAR>DecidableEq ι<VAR>f : (ι → A) →ₗ[A] ι → A<GOAL>(LinearMap.toMatrix' f).det = LinearMap.det f
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>f : Matrix ι ι R<GOAL>LinearMap.det ((Matrix.toLin b b) f) = f.det
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>f : Matrix ι ι R<GOAL>LinearMap.det (Matrix.toLin' f) = f.det
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<VAR>DecidableEq M<VAR>P : A → Prop<VAR>f : M →ₗ[A] M<VAR>hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P ((LinearMap.toMatrix b b) f).det<VAR>h1 : P 1<GOAL>P (LinearMap.det f)
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<VAR>f g : M →ₗ[A] M<GOAL>LinearMap.det (f ∘ₗ g) = LinearMap.det f * LinearMap.det g
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<GOAL>LinearMap.det LinearMap.id = 1
<VAR>𝕜 : Type u_7<VAR>Field 𝕜<VAR>M : Type u_8<VAR>AddCommGroup M<VAR>Module 𝕜 M<VAR>c : 𝕜<VAR>f : M →ₗ[𝕜] M<GOAL>LinearMap.det (c • f) = c ^ FiniteDimensional.finrank 𝕜 M * LinearMap.det f
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<VAR>ι : Type u_7<VAR>Finite ι<VAR>Nonempty ι<VAR>b : Basis ι A M<GOAL>LinearMap.det 0 = 0
<VAR>𝕜 : Type u_7<VAR>Field 𝕜<VAR>M : Type u_8<VAR>AddCommGroup M<VAR>Module 𝕜 M<GOAL>LinearMap.det 0 = 0 ^ FiniteDimensional.finrank 𝕜 M
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Subsingleton M<VAR>f : M →ₗ[R] M<GOAL>LinearMap.det f = 1
<VAR>𝕜 : Type u_7<VAR>Field 𝕜<VAR>M : Type u_8<VAR>AddCommGroup M<VAR>Module 𝕜 M<VAR>h : FiniteDimensional.finrank 𝕜 M = 0<VAR>f : M →ₗ[𝕜] M<GOAL>LinearMap.det f = 1
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<VAR>N : Type u_7<VAR>AddCommGroup N<VAR>Module A N<VAR>f : M →ₗ[A] M<VAR>e : M ≃ₗ[A] N<GOAL>LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>A : Type u_7<VAR>CommRing A<VAR>Module A M<VAR>f : M →ₗ[A] M<VAR>hf : IsUnit f<GOAL>IsUnit (LinearMap.det f)
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>𝕜 : Type u_7<VAR>Field 𝕜<VAR>Module 𝕜 M<VAR>f : M →ₗ[𝕜] M<VAR>hf : LinearMap.det f ≠ 1<GOAL>FiniteDimensional 𝕜 M
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>𝕜 : Type u_7<VAR>Field 𝕜<VAR>Module 𝕜 M<VAR>f : M →ₗ[𝕜] M<VAR>hf : LinearMap.det f = 0<GOAL>LinearMap.range f < ⊤
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>𝕜 : Type u_7<VAR>Field 𝕜<VAR>Module 𝕜 M<VAR>f : M →ₗ[𝕜] M<VAR>hf : LinearMap.det f = 0<GOAL>⊥ < LinearMap.ker f
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>f : M ≃ₗ[R] M<GOAL>↑(LinearEquiv.det f) = LinearMap.det ↑f
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>f : M ≃ₗ[R] M<GOAL>↑(LinearEquiv.det f)⁻¹ = LinearMap.det ↑f.symm
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<GOAL>LinearEquiv.det (LinearEquiv.refl R M) = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>f g : M ≃ₗ[R] M<GOAL>LinearEquiv.det (f ≪≫ₗ g) = LinearEquiv.det g * LinearEquiv.det f
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>f : M ≃ₗ[R] M<GOAL>LinearEquiv.det f.symm = LinearEquiv.det f⁻¹
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommGroup M'<VAR>Module R M'<VAR>f : M ≃ₗ[R] M<VAR>e : M ≃ₗ[R] M'<GOAL>LinearEquiv.det (e.symm ≪≫ₗ f ≪≫ₗ e) = LinearEquiv.det f
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<VAR>f : M ≃ₗ[A] M<GOAL>LinearMap.det ↑f * LinearMap.det ↑f.symm = 1
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<VAR>f : M ≃ₗ[A] M<GOAL>LinearMap.det ↑f.symm * LinearMap.det ↑f = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommGroup M'<VAR>Module R M'<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>f : M ≃ₗ[R] M'<VAR>v : Basis ι R M<VAR>v' : Basis ι R M'<GOAL>IsUnit ((LinearMap.toMatrix v v') ↑f).det
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<VAR>f : M ≃ₗ[A] M<GOAL>IsUnit (LinearMap.det ↑f)
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>𝕜 : Type u_5<VAR>Field 𝕜<VAR>Module 𝕜 M<VAR>f : M ≃ₗ[𝕜] M<GOAL>LinearMap.det ↑f.symm = (LinearMap.det ↑f)⁻¹
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommGroup M'<VAR>Module R M'<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>f : M →ₗ[R] M'<VAR>v : Basis ι R M<VAR>v' : Basis ι R M'<VAR>h : IsUnit ((LinearMap.toMatrix v v') f).det<VAR>a : M'<GOAL>(LinearEquiv.ofIsUnitDet h).symm a = ((Matrix.toLin v' v) ((LinearMap.toMatrix v v') f)⁻¹) a
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommGroup M'<VAR>Module R M'<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>f : M →ₗ[R] M'<VAR>v : Basis ι R M<VAR>v' : Basis ι R M'<VAR>h : IsUnit ((LinearMap.toMatrix v v') f).det<VAR>a : M<GOAL>(LinearEquiv.ofIsUnitDet h) a = f a
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommGroup M'<VAR>Module R M'<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>f : M →ₗ[R] M'<VAR>v : Basis ι R M<VAR>v' : Basis ι R M'<VAR>h : IsUnit ((LinearMap.toMatrix v v') f).det<GOAL>↑(LinearEquiv.ofIsUnitDet h) = f
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>e : M ≃ₗ[R] M<VAR>f f' : M →ₗ[R] M<VAR>h : ∀ (x : M), f x = f' (e x)<GOAL>Associated (LinearMap.det f) (LinearMap.det f')
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_5<VAR>AddCommGroup N<VAR>Module R N<VAR>f : N →ₗ[R] M<VAR>e e' : M ≃ₗ[R] N<GOAL>Associated (LinearMap.det (f ∘ₗ ↑e)) (LinearMap.det (f ∘ₗ ↑e'))
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>e : Basis ι R M<VAR>v : ι → M<GOAL>e.det v = (e.toMatrix v).det
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>e : Basis ι R M<GOAL>e.det ⇑e = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>e : Basis ι R M<VAR>IsEmpty ι<GOAL>e.det = AlternatingMap.constOfIsEmpty R M ι 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>e : Basis ι R M<VAR>Nontrivial R<GOAL>e.det ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>e : Basis ι R M<VAR>G : Type u_5<VAR>Group G<VAR>DistribMulAction G M<VAR>SMulCommClass G R M<VAR>g : G<VAR>v : ι → M<GOAL>(g • e).det v = e.det (g⁻¹ • v)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>e : Basis ι R M<VAR>v : ι → M<GOAL>LinearIndependent R v ∧ Submodule.span R (Set.range v) = ⊤ ↔ IsUnit (e.det v)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>e e' : Basis ι R M<GOAL>IsUnit (e.det ⇑e')
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>e : Basis ι R M<VAR>f : M [⋀^ι]→ₗ[R] R<GOAL>f = f ⇑e • e.det
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_5<VAR>Finite ι<VAR>e : Basis ι R M<VAR>f : M [⋀^ι]→ₗ[R] R<GOAL>f ⇑e = 0 ↔ f = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_5<VAR>Finite ι<VAR>e : Basis ι R M<VAR>f : M [⋀^ι]→ₗ[R] R<GOAL>f ⇑e ≠ 0 ↔ f ≠ 0
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<VAR>e : Basis ι A M<VAR>f : M →ₗ[A] M<VAR>v : ι → M<GOAL>e.det (⇑f ∘ v) = LinearMap.det f * e.det v
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>M' : Type u_3<VAR>AddCommGroup M'<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>A : Type u_5<VAR>CommRing A<VAR>Module A M<VAR>Module A M'<VAR>b : Basis ι A M<VAR>b' : Basis ι A M'<VAR>f : M →ₗ[A] M'<GOAL>b'.det (⇑f ∘ ⇑b) = LinearMap.det (f ∘ₗ ↑(b'.equiv b (Equiv.refl ι)))
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>ι' : Type u_6<VAR>Fintype ι'<VAR>DecidableEq ι'<VAR>b : Basis ι R M<VAR>v : ι' → M<VAR>e : ι ≃ ι'<GOAL>(b.reindex e).det v = b.det (v ∘ ⇑e)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>ι' : Type u_6<VAR>Fintype ι'<VAR>DecidableEq ι'<VAR>b : Basis ι R M<VAR>e : ι ≃ ι'<GOAL>(b.reindex e).det = AlternatingMap.domDomCongr e b.det
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>ι' : Type u_6<VAR>Fintype ι'<VAR>DecidableEq ι'<VAR>b : Basis ι R M<VAR>v : ι → M<VAR>e : ι' ≃ ι<GOAL>(b.reindex e.symm).det (v ∘ ⇑e) = b.det v
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommGroup M'<VAR>Module R M'<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>f : M ≃ₗ[R] M'<VAR>v : ι → M'<GOAL>(b.map f).det v = b.det (⇑f.symm ∘ v)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommGroup M'<VAR>Module R M'<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>f : M ≃ₗ[R] M'<GOAL>(b.map f).det = b.det.compLinearMap ↑f.symm
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<GOAL>(Pi.basisFun R ι).det = Matrix.detRowAlternating
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>e : Basis ι R M<VAR>v : ι → M<VAR>hli : LinearIndependent R v<VAR>hsp : ⊤ ≤ Submodule.span R (Set.range v)<VAR>i : ι<GOAL>e.det v • (Basis.mk hli hsp).coord i = (↑e.det).toLinearMap v i
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>e : Basis ι R M<VAR>w : ι → Rˣ<GOAL>(e.unitsSMul w).det = ↑(∏ i : ι, w i)⁻¹ • e.det
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>e : Basis ι R M<VAR>w : ι → Rˣ<GOAL>e.det ⇑(e.unitsSMul w) = ∏ i : ι, ↑(w i)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>e : Basis ι R M<VAR>w : ι → R<VAR>hw : ∀ (i : ι), IsUnit (w i)<GOAL>e.det ⇑(e.isUnitSMul hw) = ∏ i : ι, w i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>AddCommMonoid N<VAR>Module R N<VAR>b : Basis ι S M<VAR>c : Basis κ R N<VAR>i : ι<VAR>j : κ<GOAL>(b.tensorProduct c) (i, j) = b i ⊗ₜ[R] c j
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>AddCommMonoid N<VAR>Module R N<VAR>b : Basis ι S M<VAR>c : Basis κ R N<VAR>i : ι × κ<GOAL>(b.tensorProduct c) i = b i.1 ⊗ₜ[R] c i.2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>AddCommMonoid N<VAR>Module R N<VAR>b : Basis ι S M<VAR>c : Basis κ R N<VAR>m : M<VAR>n : N<VAR>i : ι<VAR>j : κ<GOAL>((b.tensorProduct c).repr (m ⊗ₜ[R] n)) (i, j) = (c.repr n) j • (b.repr m) i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>x : S<VAR>y : M<VAR>i : ι<GOAL>((Basis.baseChange S b).repr (x ⊗ₜ[R] y)) i = (b.repr y) i • x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>i : ι<GOAL>(Basis.baseChange S b) i = 1 ⊗ₜ[R] b i
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₃<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>m₃ : M₃<GOAL>(TensorProduct.prodRight R M₁ M₂ M₃) (m₁ ⊗ₜ[R] (m₂, m₃)) = (m₁ ⊗ₜ[R] m₂, m₁ ⊗ₜ[R] m₃)
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₃<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>m₃ : M₃<GOAL>(TensorProduct.prodRight R M₁ M₂ M₃).symm (m₁ ⊗ₜ[R] m₂, m₁ ⊗ₜ[R] m₃) = m₁ ⊗ₜ[R] (m₂, m₃)
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₃<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>m₃ : M₃<GOAL>(TensorProduct.prodLeft R M₁ M₂ M₃) ((m₁, m₂) ⊗ₜ[R] m₃) = (m₁ ⊗ₜ[R] m₃, m₂ ⊗ₜ[R] m₃)
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₃<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>m₃ : M₃<GOAL>(TensorProduct.prodLeft R M₁ M₂ M₃).symm (m₁ ⊗ₜ[R] m₃, m₂ ⊗ₜ[R] m₃) = (m₁, m₂) ⊗ₜ[R] m₃
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>x : M ⊗[R] N<GOAL>∃ S, x = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) S).sum
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>x : M ⊗[R] N<GOAL>∃ S, x = S.sum fun m n => m ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>x : M ⊗[R] N<GOAL>∃ S, x = S.sum fun n m => m ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>x : M ⊗[R] N<GOAL>∃ S, x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>s : Set (M ⊗[R] N)<VAR>hs : s.Finite<GOAL>∃ M' N', Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (TensorProduct.mapIncl M' N'))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>s : Set (M ⊗[R] N)<VAR>hs : s.Finite<GOAL>∃ M', Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.range (LinearMap.rTensor N M'.subtype))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>s : Set (M ⊗[R] N)<VAR>hs : s.Finite<GOAL>∃ N', Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (LinearMap.lTensor M N'.subtype))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>M₁ : Submodule R M<VAR>N₁ : Submodule R N<VAR>s : Set (↥M₁ ⊗[R] ↥N₁)<VAR>hs : s.Finite<GOAL>∃ M' N', ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁), Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (TensorProduct.map (Submodule.inclusion hM) (Submodule.inclusion hN)))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>M₁ : Submodule R M<VAR>N₁ : Submodule R N<VAR>s : Set (↥M₁ ⊗[R] ↥N₁)<VAR>hs : s.Finite<GOAL>∃ M', ∃ (hM : M' ≤ M₁), Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N₁) (Submodule.inclusion hM)))