internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.generize_finsupp_eq
Proof state before:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
⊢ (h.sum fun k n =>
      (∏ i : ι, (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (∑ i : ι, X i ⊗ₜ[R] b i) ^ k i) ⊗ₜ[R] n) =
    h.sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Tactic:
simp only [this]
Proof state after:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
⊢ (h.sum fun k n => (∏ x : ι, X x ^ k x) ⊗ₜ[R] n) = h.sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Theorem: PolynomialMap.generize_finsupp_eq
Proof state before:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
⊢ (h.sum fun k n => (∏ x : ι, X x ^ k x) ⊗ₜ[R] n) = h.sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Tactic:
apply Finsupp.sum_congr
Proof state after:
case h
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
⊢ ∀ x ∈ h.support, (∏ x_1 : ι, X x_1 ^ x x_1) ⊗ₜ[R] h x = (monomial x) 1 ⊗ₜ[R] h x
Theorem: PolynomialMap.generize_finsupp_eq
Proof state before:
case h
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
⊢ ∀ x ∈ h.support, (∏ x_1 : ι, X x_1 ^ x x_1) ⊗ₜ[R] h x = (monomial x) 1 ⊗ₜ[R] h x
Tactic:
intro k _
Proof state after:
case h
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ (∏ x : ι, X x ^ k x) ⊗ₜ[R] h k = (monomial k) 1 ⊗ₜ[R] h k
Theorem: PolynomialMap.generize_finsupp_eq
Proof state before:
case h
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ (∏ x : ι, X x ^ k x) ⊗ₜ[R] h k = (monomial k) 1 ⊗ₜ[R] h k
Tactic:
congr
Proof state after:
case h.e_m
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∏ x : ι, X x ^ k x = (monomial k) 1
Theorem: PolynomialMap.generize_finsupp_eq
Proof state before:
case h.e_m
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∏ x : ι, X x ^ k x = (monomial k) 1
Tactic:
rw [← MvPolynomial.prod_X_pow_eq_monomial, ← prod_mul_prod_compl k.support]
Proof state after:
case h.e_m
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ (∏ i ∈ k.support, X i ^ k i) * ∏ i ∈ k.supportᶜ, X i ^ k i = ∏ x ∈ k.support, X x ^ k x
Theorem: PolynomialMap.generize_finsupp_eq
Proof state before:
case h.e_m
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ (∏ i ∈ k.support, X i ^ k i) * ∏ i ∈ k.supportᶜ, X i ^ k i = ∏ x ∈ k.support, X x ^ k x
Tactic:
convert mul_one _
Proof state after:
case h.e'_2.h.e'_6
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∏ i ∈ k.supportᶜ, X i ^ k i = 1
Theorem: PolynomialMap.generize_finsupp_eq
Proof state before:
case h.e'_2.h.e'_6
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∏ i ∈ k.supportᶜ, X i ^ k i = 1
Tactic:
apply prod_eq_one
Proof state after:
case h.e'_2.h.e'_6.h
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∀ x ∈ k.supportᶜ, X x ^ k x = 1
Theorem: PolynomialMap.generize_finsupp_eq
Proof state before:
case h.e'_2.h.e'_6.h
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∀ x ∈ k.supportᶜ, X x ^ k x = 1
Tactic:
intro i hi
Proof state after:
case h.e'_2.h.e'_6.h
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
i : ι
hi : i ∈ k.supportᶜ
⊢ X i ^ k i = 1
Theorem: PolynomialMap.generize_finsupp_eq
Proof state before:
case h.e'_2.h.e'_6.h
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
i : ι
hi : i ∈ k.supportᶜ
⊢ X i ^ k i = 1
Tactic:
rw [mem_compl, Finsupp.mem_support_iff, ne_eq, not_not] at hi
Proof state after:
case h.e'_2.h.e'_6.h
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
i : ι
hi : k i = 0
⊢ X i ^ k i = 1
Theorem: PolynomialMap.generize_finsupp_eq
Proof state before:
case h.e'_2.h.e'_6.h
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
i : ι
hi : k i = 0
⊢ X i ^ k i = 1
Tactic:
rw [hi, pow_zero]
Proof state after:
no goals
Theorem: PolynomialMap.generize_finsupp_eq
Proof state before:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
⊢ (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
Tactic:
rw [hm, map_sum, sum_eq_single i, LinearForm.baseChange_apply_tmul, Basis.coord_apply,
  Basis.repr_self, Finsupp.single_eq_same, _root_.one_smul, mul_one]
Proof state after:
case h₀
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
⊢ ∀ b_1 ∈ univ, b_1 ≠ i → (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (X b_1 ⊗ₜ[R] b b_1) = 0

case h₁
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
⊢ i ∉ univ → (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (X i ⊗ₜ[R] b i) = 0
Theorem: PolynomialMap.generize_finsupp_eq
Proof state before:
case h₀
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
⊢ ∀ b_1 ∈ univ, b_1 ≠ i → (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (X b_1 ⊗ₜ[R] b b_1) = 0
Tactic:
intro j _ hj
Proof state after:
case h₀
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i j : ι
a✝ : j ∈ univ
hj : j ≠ i
⊢ (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (X j ⊗ₜ[R] b j) = 0
Theorem: PolynomialMap.generize_finsupp_eq
Proof state before:
case h₀
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i j : ι
a✝ : j ∈ univ
hj : j ≠ i
⊢ (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (X j ⊗ₜ[R] b j) = 0
Tactic:
rw [LinearForm.baseChange_apply_tmul, Basis.coord_apply,
  Basis.repr_self, Algebra.mul_smul_comm, mul_one, Finsupp.single_smul,
  _root_.one_smul, Finsupp.single_eq_of_ne hj]
Proof state after:
no goals
Theorem: PolynomialMap.generize_finsupp_eq
Proof state before:
case h₁
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
⊢ i ∉ univ → (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (X i ⊗ₜ[R] b i) = 0
Tactic:
intro hi
Proof state after:
case h₁
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
hi : i ∉ univ
⊢ (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (X i ⊗ₜ[R] b i) = 0
Theorem: PolynomialMap.generize_finsupp_eq
Proof state before:
case h₁
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
hi : i ∉ univ
⊢ (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (X i ⊗ₜ[R] b i) = 0
Tactic:
exfalso
Proof state after:
case h₁
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
hi : i ∉ univ
⊢ False
Theorem: PolynomialMap.generize_finsupp_eq
Proof state before:
case h₁
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
hi : i ∉ univ
⊢ False
Tactic:
exact hi (mem_univ _)
Proof state after:
no goals
Theorem: PolynomialMap.coeff_of_finsupp_polynomialMap
Proof state before:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
⊢ (coeff ⇑b) (Finsupp.polynomialMap b h) = h
Tactic:
simp only [coeff, coe_mk, AddHom.coe_mk, coe_comp, LinearEquiv.coe_coe, Function.comp_apply]
Proof state after:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
⊢ scalarRTensor ((generize ⇑b) (Finsupp.polynomialMap b h)) = h
Theorem: PolynomialMap.coeff_of_finsupp_polynomialMap
Proof state before:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
⊢ scalarRTensor ((generize ⇑b) (Finsupp.polynomialMap b h)) = h
Tactic:
ext d
Proof state after:
case h
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
d : ι →₀ ℕ
⊢ (scalarRTensor ((generize ⇑b) (Finsupp.polynomialMap b h))) d = h d
Theorem: PolynomialMap.coeff_of_finsupp_polynomialMap
Proof state before:
case h
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
d : ι →₀ ℕ
⊢ (scalarRTensor ((generize ⇑b) (Finsupp.polynomialMap b h))) d = h d
Tactic:
rw [scalarRTensor_apply, eq_comm, ← LinearEquiv.symm_apply_eq, TensorProduct.lid_symm_apply,
  generize_finsupp_eq, map_finsupp_sum, Finsupp.sum_eq_single d
  (fun b _ hb => by rw [rTensor_tmul, lcoeff_apply, coeff_monomial, if_neg hb, zero_tmul])
  (fun _ => by rw [tmul_zero, map_zero]), rTensor_tmul, lcoeff_apply, coeff_monomial, if_pos rfl]
Proof state after:
no goals
Theorem: PolynomialMap.coeff_of_finsupp_polynomialMap
Proof state before:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝¹ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b✝ : Basis ι R M
h : (ι →₀ ℕ) →₀ N
d b : ι →₀ ℕ
x✝ : h b ≠ 0
hb : b ≠ d
⊢ (LinearMap.rTensor N (lcoeff R d)) ((monomial b) 1 ⊗ₜ[R] h b) = 0
Tactic:
rw [rTensor_tmul, lcoeff_apply, coeff_monomial, if_neg hb, zero_tmul]
Proof state after:
no goals
Theorem: PolynomialMap.coeff_of_finsupp_polynomialMap
Proof state before:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
d : ι →₀ ℕ
x✝ : h d = 0
⊢ (LinearMap.rTensor N (lcoeff R d)) ((monomial d) 1 ⊗ₜ[R] 0) = 0
Tactic:
rw [tmul_zero, map_zero]
Proof state after:
no goals