internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.rTensorAlgHom_toLinearMap
Proof state before:
case a.h.h.h.a
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e (((AlgebraTensorModule.curry rTensorAlgHom.toLinearMap ∘ₗ monomial d) 1) n) =
    coeff e (((AlgebraTensorModule.curry ↑(finsuppLeft' R S N (σ →₀ ℕ) S) ∘ₗ monomial d) 1) n)
Tactic:
simp only [coe_comp, Function.comp_apply, AlgebraTensorModule.curry_apply, curry_apply,
  LinearMap.coe_restrictScalars, AlgHom.toLinearMap_apply]
Proof state after:
case a.h.h.h.a
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e (rTensorAlgHom ((monomial d) 1 ⊗ₜ[R] n)) = coeff e (↑(finsuppLeft' R S N (σ →₀ ℕ) S) ((monomial d) 1 ⊗ₜ[R] n))
Theorem: MvPolynomial.rTensorAlgHom_toLinearMap
Proof state before:
case a.h.h.h.a
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e (rTensorAlgHom ((monomial d) 1 ⊗ₜ[R] n)) = coeff e (↑(finsuppLeft' R S N (σ →₀ ℕ) S) ((monomial d) 1 ⊗ₜ[R] n))
Tactic:
rw [rTensorAlgHom_coeff_tmul]
Proof state after:
case a.h.h.h.a
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e ((monomial d) 1) ⊗ₜ[R] n = coeff e (↑(finsuppLeft' R S N (σ →₀ ℕ) S) ((monomial d) 1 ⊗ₜ[R] n))
Theorem: MvPolynomial.rTensorAlgHom_toLinearMap
Proof state before:
case a.h.h.h.a
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e ((monomial d) 1) ⊗ₜ[R] n = coeff e (↑(finsuppLeft' R S N (σ →₀ ℕ) S) ((monomial d) 1 ⊗ₜ[R] n))
Tactic:
simp only [coeff]
Proof state after:
case a.h.h.h.a
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ ((monomial d) 1) e ⊗ₜ[R] n = (↑(finsuppLeft' R S N (σ →₀ ℕ) S) ((monomial d) 1 ⊗ₜ[R] n)) e
Theorem: MvPolynomial.rTensorAlgHom_toLinearMap
Proof state before:
case a.h.h.h.a
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ ((monomial d) 1) e ⊗ₜ[R] n = (↑(finsuppLeft' R S N (σ →₀ ℕ) S) ((monomial d) 1 ⊗ₜ[R] n)) e
Tactic:
erw [finsuppLeft_apply_tmul_apply]
Proof state after:
no goals
Theorem: MvPolynomial.rTensorAlgHom_toLinearMap'
Proof state before:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
⊢ ↑R rTensorAlgHom.toLinearMap = ↑(finsuppLeft R S N (σ →₀ ℕ))
Tactic:
rw [rTensorAlgHom_toLinearMap]
Proof state after:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
⊢ ↑R ↑(finsuppLeft' R S N (σ →₀ ℕ) S) = ↑(finsuppLeft R S N (σ →₀ ℕ))
Theorem: MvPolynomial.rTensorAlgHom_toLinearMap'
Proof state before:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
⊢ ↑R ↑(finsuppLeft' R S N (σ →₀ ℕ) S) = ↑(finsuppLeft R S N (σ →₀ ℕ))
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPolynomial.rTensorAlgHom_apply_eq
Proof state before:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S ⊗[R] N
⊢ rTensorAlgHom p = (finsuppLeft' R S N (σ →₀ ℕ) S) p
Tactic:
rw [← AlgHom.toLinearMap_apply, rTensorAlgHom_toLinearMap]
Proof state after:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S ⊗[R] N
⊢ ↑(finsuppLeft' R S N (σ →₀ ℕ) S) p = (finsuppLeft' R S N (σ →₀ ℕ) S) p
Theorem: MvPolynomial.rTensorAlgHom_apply_eq
Proof state before:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S ⊗[R] N
⊢ ↑(finsuppLeft' R S N (σ →₀ ℕ) S) p = (finsuppLeft' R S N (σ →₀ ℕ) S) p
Tactic:
rfl
Proof state after:
no goals
Theorem: Polynomial.scalarRTensor_apply_tmul_apply
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((scalarRTensor R N) (p ⊗ₜ[R] n)) i = p.coeff i • n
Tactic:
simp only [scalarRTensor, LinearEquiv.trans_apply]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((finsuppScalarLeft R N ℕ) ((LinearEquiv.rTensor N (toFinsuppLinearEquiv R)) (p ⊗ₜ[R] n))) i = p.coeff i • n
Theorem: Polynomial.scalarRTensor_apply_tmul_apply
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((finsuppScalarLeft R N ℕ) ((LinearEquiv.rTensor N (toFinsuppLinearEquiv R)) (p ⊗ₜ[R] n))) i = p.coeff i • n
Tactic:
simp only [LinearEquiv.rTensor, congr_tmul, refl_apply]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((finsuppScalarLeft R N ℕ) ((toFinsuppLinearEquiv R) p ⊗ₜ[R] n)) i = p.coeff i • n
Theorem: Polynomial.scalarRTensor_apply_tmul_apply
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((finsuppScalarLeft R N ℕ) ((toFinsuppLinearEquiv R) p ⊗ₜ[R] n)) i = p.coeff i • n
Tactic:
rw [finsuppScalarLeft_apply_tmul_apply _ n i]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((toFinsuppLinearEquiv R) p) i • n = p.coeff i • n
Theorem: Polynomial.scalarRTensor_apply_tmul_apply
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((toFinsuppLinearEquiv R) p) i • n = p.coeff i • n
Tactic:
rfl
Proof state after:
no goals
Theorem: Polynomial.scalarRTensor_apply_tmul
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
⊢ (scalarRTensor R N) (p ⊗ₜ[R] n) = p.sum fun i r => Finsupp.single i (r • n)
Tactic:
ext i
Proof state after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((scalarRTensor R N) (p ⊗ₜ[R] n)) i = (p.sum fun i r => Finsupp.single i (r • n)) i
Theorem: Polynomial.scalarRTensor_apply_tmul
Proof state before:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((scalarRTensor R N) (p ⊗ₜ[R] n)) i = (p.sum fun i r => Finsupp.single i (r • n)) i
Tactic:
rw [scalarRTensor_apply_tmul_apply]
Proof state after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ p.coeff i • n = (p.sum fun i r => Finsupp.single i (r • n)) i
Theorem: Polynomial.scalarRTensor_apply_tmul
Proof state before:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ p.coeff i • n = (p.sum fun i r => Finsupp.single i (r • n)) i
Tactic:
rw [sum_def]
Proof state after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ p.coeff i • n = (∑ n_1 ∈ p.support, Finsupp.single n_1 (p.coeff n_1 • n)) i
Theorem: Polynomial.scalarRTensor_apply_tmul
Proof state before:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ p.coeff i • n = (∑ n_1 ∈ p.support, Finsupp.single n_1 (p.coeff n_1 • n)) i
Tactic:
rw [Finset.sum_apply']
Proof state after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ p.coeff i • n = ∑ k ∈ p.support, (Finsupp.single k (p.coeff k • n)) i
Theorem: Polynomial.scalarRTensor_apply_tmul
Proof state before:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ p.coeff i • n = ∑ k ∈ p.support, (Finsupp.single k (p.coeff k • n)) i
Tactic:
rw [Finset.sum_eq_single i]
Proof state after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ p.coeff i • n = (Finsupp.single i (p.coeff i • n)) i

case h.h₀
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ∀ b ∈ p.support, b ≠ i → (Finsupp.single b (p.coeff b • n)) i = 0

case h.h₁
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ i ∉ p.support → (Finsupp.single i (p.coeff i • n)) i = 0
Theorem: Polynomial.scalarRTensor_apply_tmul
Proof state before:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ p.coeff i • n = (Finsupp.single i (p.coeff i • n)) i
Tactic:
simp only [Finsupp.single_eq_same]
Proof state after:
no goals
Theorem: Polynomial.scalarRTensor_apply_tmul
Proof state before:
case h.h₀
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ∀ b ∈ p.support, b ≠ i → (Finsupp.single b (p.coeff b • n)) i = 0
Tactic:
exact fun _ _ => Finsupp.single_eq_of_ne
Proof state after:
no goals
Theorem: Polynomial.scalarRTensor_apply_tmul
Proof state before:
case h.h₁
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ i ∉ p.support → (Finsupp.single i (p.coeff i • n)) i = 0
Tactic:
intro h
Proof state after:
case h.h₁
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
h : i ∉ p.support
⊢ (Finsupp.single i (p.coeff i • n)) i = 0
Theorem: Polynomial.scalarRTensor_apply_tmul
Proof state before:
case h.h₁
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
h : i ∉ p.support
⊢ (Finsupp.single i (p.coeff i • n)) i = 0
Tactic:
simp only [mem_support_iff, ne_eq, not_not] at h
Proof state after:
case h.h₁
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
h : p.coeff i = 0
⊢ (Finsupp.single i (p.coeff i • n)) i = 0
Theorem: Polynomial.scalarRTensor_apply_tmul
Proof state before:
case h.h₁
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
h : p.coeff i = 0
⊢ (Finsupp.single i (p.coeff i • n)) i = 0
Tactic:
rw [h, zero_smul, Finsupp.single_zero, Finsupp.coe_zero, Pi.zero_apply]
Proof state after:
no goals
Theorem: Polynomial.scalarRTensor_apply
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
pn : R[X] ⊗[R] N
d : ℕ
⊢ ((scalarRTensor R N) pn) d = (TensorProduct.lid R N) ((LinearMap.rTensor N (lcoeff R d)) pn)
Tactic:
rw [← LinearEquiv.symm_apply_eq, lid_symm_apply]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
pn : R[X] ⊗[R] N
d : ℕ
⊢ 1 ⊗ₜ[R] ((scalarRTensor R N) pn) d = (LinearMap.rTensor N (lcoeff R d)) pn
Theorem: Polynomial.scalarRTensor_apply
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
pn : R[X] ⊗[R] N
d : ℕ
⊢ 1 ⊗ₜ[R] ((scalarRTensor R N) pn) d = (LinearMap.rTensor N (lcoeff R d)) pn
Tactic:
induction pn using TensorProduct.induction_on with
| zero => simp
| tmul p n => simp [scalarRTensor_apply_tmul_apply, TensorProduct.smul_tmul']
| add x y hx hy => simp [tmul_add, hx, hy]
Proof state after:
no goals
Theorem: Polynomial.scalarRTensor_apply
Proof state before:
case zero
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
d : ℕ
⊢ 1 ⊗ₜ[R] ((scalarRTensor R N) 0) d = (LinearMap.rTensor N (lcoeff R d)) 0
Tactic:
simp
Proof state after:
no goals
Theorem: Polynomial.scalarRTensor_apply
Proof state before:
case tmul
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
d : ℕ
p : R[X]
n : N
⊢ 1 ⊗ₜ[R] ((scalarRTensor R N) (p ⊗ₜ[R] n)) d = (LinearMap.rTensor N (lcoeff R d)) (p ⊗ₜ[R] n)
Tactic:
simp [scalarRTensor_apply_tmul_apply, TensorProduct.smul_tmul']
Proof state after:
no goals
Theorem: Polynomial.scalarRTensor_apply
Proof state before:
case add
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
d : ℕ
x y : R[X] ⊗[R] N
hx : 1 ⊗ₜ[R] ((scalarRTensor R N) x) d = (LinearMap.rTensor N (lcoeff R d)) x
hy : 1 ⊗ₜ[R] ((scalarRTensor R N) y) d = (LinearMap.rTensor N (lcoeff R d)) y
⊢ 1 ⊗ₜ[R] ((scalarRTensor R N) (x + y)) d = (LinearMap.rTensor N (lcoeff R d)) (x + y)
Tactic:
simp [tmul_add, hx, hy]
Proof state after:
no goals
Theorem: Polynomial.rTensor_apply_tmul_apply
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
i : ℕ
⊢ ((rTensor R N S) (p ⊗ₜ[R] n)) i = p.coeff i ⊗ₜ[R] n
Tactic:
simp only [rTensor, LinearEquiv.trans_apply, finsuppLeft'_apply]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
i : ℕ
⊢ ((finsuppLeft R S N ℕ) ((rTensor' N (toFinsuppLinearEquiv S)) (p ⊗ₜ[R] n))) i = p.coeff i ⊗ₜ[R] n
Theorem: Polynomial.rTensor_apply_tmul_apply
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
i : ℕ
⊢ ((finsuppLeft R S N ℕ) ((rTensor' N (toFinsuppLinearEquiv S)) (p ⊗ₜ[R] n))) i = p.coeff i ⊗ₜ[R] n
Tactic:
simp only [LinearEquiv.rTensor'_apply, LinearEquiv.rTensor, congr_tmul,
  LinearEquiv.restrictScalars_apply, LinearEquiv.refl_apply]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
i : ℕ
⊢ ((finsuppLeft R S N ℕ) ((toFinsuppLinearEquiv S) p ⊗ₜ[R] n)) i = p.coeff i ⊗ₜ[R] n
Theorem: Polynomial.rTensor_apply_tmul_apply
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
i : ℕ
⊢ ((finsuppLeft R S N ℕ) ((toFinsuppLinearEquiv S) p ⊗ₜ[R] n)) i = p.coeff i ⊗ₜ[R] n
Tactic:
simp only [toFinsuppLinearEquiv, RingEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe,
  Equiv.invFun_as_coe, LinearEquiv.coe_mk, toFinsuppIso_apply]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
i : ℕ
⊢ ((finsuppLeft R S N ℕ) (p.toFinsupp ⊗ₜ[R] n)) i = p.coeff i ⊗ₜ[R] n
Theorem: Polynomial.rTensor_apply_tmul_apply
Proof state before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
i : ℕ
⊢ ((finsuppLeft R S N ℕ) (p.toFinsupp ⊗ₜ[R] n)) i = p.coeff i ⊗ₜ[R] n
Tactic:
rw [finsuppLeft_apply_tmul_apply]
Proof state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
i : ℕ
⊢ p.toFinsupp i ⊗ₜ[R] n = p.coeff i ⊗ₜ[R] n