internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof state before:
case hnc.h
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
b : ι →₀ ℕ
a✝ : ((coeff fun i => m i) f) b ≠ 0
hb' : b ≠ d
h : e b (∑ i : ι, b i) = e d (d.sum fun x n => n)
i : ι
⊢ b i = d i
Tactic:
rw [← he_some b _ i, h]
Proof state after:
case hnc.h
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
b : ι →₀ ℕ
a✝ : ((coeff fun i => m i) f) b ≠ 0
hb' : b ≠ d
h : e b (∑ i : ι, b i) = e d (d.sum fun x n => n)
i : ι
⊢ (e d (d.sum fun x n => n)) (some i) = d i
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof state before:
case hnc.h
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
b : ι →₀ ℕ
a✝ : ((coeff fun i => m i) f) b ≠ 0
hb' : b ≠ d
h : e b (∑ i : ι, b i) = e d (d.sum fun x n => n)
i : ι
⊢ (e d (d.sum fun x n => n)) (some i) = d i
Tactic:
exact he_some d _ i
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegree_of_coeff_iff
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
⊢ IsHomogeneousOfDegree p f ↔ ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
Tactic:
refine ⟨fun hf _ m d hd => isHomogeneousOfDegree_coeff hf m d hd, fun H S _ _ r μ => ?_⟩
Proof state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
μ : S ⊗[R] M
⊢ f.toFun' S (r • μ) = r ^ p • f.toFun' S μ
Theorem: PolynomialMap.isHomogeneousOfDegree_of_coeff_iff
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
μ : S ⊗[R] M
⊢ f.toFun' S (r • μ) = r ^ p • f.toFun' S μ
Tactic:
obtain ⟨n, s, m, rfl⟩ := TensorProduct.exists_Fin S μ
Proof state after:
case intro.intro.intro
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
⊢ f.toFun' S (r • ∑ i : Fin n, s i ⊗ₜ[R] m i) = r ^ p • f.toFun' S (∑ i : Fin n, s i ⊗ₜ[R] m i)
Theorem: PolynomialMap.isHomogeneousOfDegree_of_coeff_iff
Proof state before:
case intro.intro.intro
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
⊢ f.toFun' S (r • ∑ i : Fin n, s i ⊗ₜ[R] m i) = r ^ p • f.toFun' S (∑ i : Fin n, s i ⊗ₜ[R] m i)
Tactic:
simp only [Finset.smul_sum, TensorProduct.smul_tmul']
Proof state after:
case intro.intro.intro
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
⊢ f.toFun' S (∑ x : Fin n, (r • s x) ⊗ₜ[R] m x) = r ^ p • f.toFun' S (∑ i : Fin n, s i ⊗ₜ[R] m i)
Theorem: PolynomialMap.isHomogeneousOfDegree_of_coeff_iff
Proof state before:
case intro.intro.intro
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
⊢ f.toFun' S (∑ x : Fin n, (r • s x) ⊗ₜ[R] m x) = r ^ p • f.toFun' S (∑ i : Fin n, s i ⊗ₜ[R] m i)
Tactic:
rw [← toFun_eq_toFun', image_eq_coeff_sum, image_eq_coeff_sum, Finsupp.smul_sum]
Proof state after:
case intro.intro.intro
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
⊢ (((coeff fun x => m x) f).sum fun k n_1 => (∏ i : Fin n, (r • s i) ^ k i) ⊗ₜ[R] n_1) =
    ((coeff fun i => m i) f).sum fun a b => r ^ p • (∏ i : Fin n, s i ^ a i) ⊗ₜ[R] b
Theorem: PolynomialMap.isHomogeneousOfDegree_of_coeff_iff
Proof state before:
case intro.intro.intro
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
⊢ (((coeff fun x => m x) f).sum fun k n_1 => (∏ i : Fin n, (r • s i) ^ k i) ⊗ₜ[R] n_1) =
    ((coeff fun i => m i) f).sum fun a b => r ^ p • (∏ i : Fin n, s i ^ a i) ⊗ₜ[R] b
Tactic:
apply Finsupp.sum_congr
Proof state after:
case intro.intro.intro.h
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
⊢ ∀ x ∈ ((coeff fun x => m x) f).support,
    (∏ i : Fin n, (r • s i) ^ x i) ⊗ₜ[R] ((coeff fun x => m x) f) x =
      r ^ p • (∏ i : Fin n, s i ^ x i) ⊗ₜ[R] ((coeff fun x => m x) f) x
Theorem: PolynomialMap.isHomogeneousOfDegree_of_coeff_iff
Proof state before:
case intro.intro.intro.h
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
⊢ ∀ x ∈ ((coeff fun x => m x) f).support,
    (∏ i : Fin n, (r • s i) ^ x i) ⊗ₜ[R] ((coeff fun x => m x) f) x =
      r ^ p • (∏ i : Fin n, s i ^ x i) ⊗ₜ[R] ((coeff fun x => m x) f) x
Tactic:
intro d hd
Proof state after:
case intro.intro.intro.h
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ (∏ i : Fin n, (r • s i) ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d =
    r ^ p • (∏ i : Fin n, s i ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d
Theorem: PolynomialMap.isHomogeneousOfDegree_of_coeff_iff
Proof state before:
case intro.intro.intro.h
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ (∏ i : Fin n, (r • s i) ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d =
    r ^ p • (∏ i : Fin n, s i ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d
Tactic:
rw [TensorProduct.smul_tmul']
Proof state after:
case intro.intro.intro.h
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ (∏ i : Fin n, (r • s i) ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d =
    (r ^ p • ∏ i : Fin n, s i ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d
Theorem: PolynomialMap.isHomogeneousOfDegree_of_coeff_iff
Proof state before:
case intro.intro.intro.h
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ (∏ i : Fin n, (r • s i) ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d =
    (r ^ p • ∏ i : Fin n, s i ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d
Tactic:
apply congr_arg₂ _ _ rfl
Proof state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ ∏ i : Fin n, (r • s i) ^ d i = r ^ p • ∏ i : Fin n, s i ^ d i
Theorem: PolynomialMap.isHomogeneousOfDegree_of_coeff_iff
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ ∏ i : Fin n, (r • s i) ^ d i = r ^ p • ∏ i : Fin n, s i ^ d i
Tactic:
simp only [smul_eq_mul, mul_pow, Finset.prod_mul_distrib]
Proof state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ (∏ x : Fin n, r ^ d x) * ∏ x : Fin n, s x ^ d x = r ^ p * ∏ i : Fin n, s i ^ d i
Theorem: PolynomialMap.isHomogeneousOfDegree_of_coeff_iff
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ (∏ x : Fin n, r ^ d x) * ∏ x : Fin n, s x ^ d x = r ^ p * ∏ i : Fin n, s i ^ d i
Tactic:
apply congr_arg₂ _ _ rfl
Proof state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ ∏ x : Fin n, r ^ d x = r ^ p
Theorem: PolynomialMap.isHomogeneousOfDegree_of_coeff_iff
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ ∏ x : Fin n, r ^ d x = r ^ p
Tactic:
rw [Finset.prod_pow_eq_pow_sum]
Proof state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ r ^ ∑ i : Fin n, d i = r ^ p
Theorem: PolynomialMap.isHomogeneousOfDegree_of_coeff_iff
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ r ^ ∑ i : Fin n, d i = r ^ p
Tactic:
apply congr_arg₂ _ rfl
Proof state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ ∑ i : Fin n, d i = p
Theorem: PolynomialMap.isHomogeneousOfDegree_of_coeff_iff
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ ∑ i : Fin n, d i = p
Tactic:
specialize H n m d
Proof state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
H : (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
⊢ ∑ i : Fin n, d i = p
Theorem: PolynomialMap.isHomogeneousOfDegree_of_coeff_iff
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
H : (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
⊢ ∑ i : Fin n, d i = p
Tactic:
rw [not_imp_comm, Finsupp.sum_of_support_subset _ (Finset.subset_univ _) _ (fun _ _ ↦ rfl)] at H
Proof state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
H : ¬((coeff m) f) d = 0 → ∑ x : Fin n, d x = p
⊢ ∑ i : Fin n, d i = p
Theorem: PolynomialMap.isHomogeneousOfDegree_of_coeff_iff
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
H : ¬((coeff m) f) d = 0 → ∑ x : Fin n, d x = p
⊢ ∑ i : Fin n, d i = p
Tactic:
exact H (Finsupp.mem_support_iff.mp hd)
Proof state after:
no goals
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
⊢ (d.sum fun x n => n) = 1 ↔ ∃ a, Finsupp.single a 1 = d
Tactic:
constructor
Proof state after:
case mp
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
⊢ (d.sum fun x n => n) = 1 → ∃ a, Finsupp.single a 1 = d

case mpr
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
⊢ (∃ a, Finsupp.single a 1 = d) → (d.sum fun x n => n) = 1
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case mp
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
⊢ (d.sum fun x n => n) = 1 → ∃ a, Finsupp.single a 1 = d
Tactic:
intro h1
Proof state after:
case mp
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
⊢ ∃ a, Finsupp.single a 1 = d
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case mp
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
⊢ ∃ a, Finsupp.single a 1 = d
Tactic:
have hd0 : d ≠ 0 := by
  intro h
  simp only [h, Finsupp.sum_zero_index, zero_ne_one] at h1
Proof state after:
case mp
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
⊢ ∃ a, Finsupp.single a 1 = d
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case mp
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
⊢ ∃ a, Finsupp.single a 1 = d
Tactic:
obtain ⟨a, ha⟩ := Finsupp.ne_iff.mp hd0
Proof state after:
case mp.intro
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
a : α
ha : d a ≠ 0 a
⊢ ∃ a, Finsupp.single a 1 = d
Theorem: PolynomialMap.Finsupp.sum_eq_one_iff
Proof state before:
case mp.intro
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
a : α
ha : d a ≠ 0 a
⊢ ∃ a, Finsupp.single a 1 = d
Tactic:
rw [Finsupp.coe_zero, Pi.zero_apply, ne_eq] at ha
Proof state after:
case mp.intro
R : Type u
inst✝⁵ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
α : Type u_3
inst✝ : DecidableEq α
d : α →₀ ℕ
h1 : (d.sum fun x n => n) = 1
hd0 : d ≠ 0
a : α
ha : ¬d a = 0
⊢ ∃ a, Finsupp.single a 1 = d