internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
case intro
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
this : m ≤ s.card
m' : ℕ
hm' : s.card = m + m'
⊢ (constantCoeff σ α) f ^ s.card = 0
Tactic:
rw [hm', pow_add, hf, MulZeroClass.zero_mul]
Proof state after:
no goals
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
⊢ ∀ i ∈ s, degree (k i) = 0
Tactic:
intro i hi
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
i : ℕ
hi : i ∈ s
⊢ degree (k i) = 0
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
i : ℕ
hi : i ∈ s
⊢ degree (k i) = 0
Tactic:
simp only [hs_def, mem_filter] at hi
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
i : ℕ
hi : i ∈ range n ∧ k i = 0
⊢ degree (k i) = 0
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
i : ℕ
hi : i ∈ range n ∧ k i = 0
⊢ degree (k i) = 0
Tactic:
rw [hi.2, map_zero]
Proof state after:
no goals
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
case convert_2
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
⊢ ∀ x ∈ range n \ s, 1 ≤ degree (k x)
Tactic:
simp only [hs_def, mem_filter, mem_sdiff, mem_range, not_and, and_imp]
Proof state after:
case convert_2
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
⊢ ∀ x < n, (x < n → ¬k x = 0) → 1 ≤ degree (k x)
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
case convert_2
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
⊢ ∀ x < n, (x < n → ¬k x = 0) → 1 ≤ degree (k x)
Tactic:
intro i hi hi'
Proof state after:
case convert_2
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
⊢ 1 ≤ degree (k i)
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
case convert_2
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
⊢ 1 ≤ degree (k i)
Tactic:
rw [← not_lt]
Proof state after:
case convert_2
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
⊢ ¬degree (k i) < 1
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
case convert_2
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
⊢ ¬degree (k i) < 1
Tactic:
intro h
Proof state after:
case convert_2
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
h : degree (k i) < 1
⊢ False
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
case convert_2
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
h : degree (k i) < 1
⊢ False
Tactic:
apply hi' hi
Proof state after:
case convert_2
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
h : degree (k i) < 1
⊢ k i = 0
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
case convert_2
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
h : degree (k i) < 1
⊢ k i = 0
Tactic:
simpa only [Nat.lt_one_iff, degree_eq_zero_iff] using h
Proof state after:
no goals
Theorem: factorial_isUnit
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
⊢ IsUnit ↑m !
Tactic:
apply isUnit_of_dvd_unit _ hn_fac
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
⊢ ↑m ! ∣ ↑(n - 1)!
Theorem: factorial_isUnit
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
⊢ ↑m ! ∣ ↑(n - 1)!
Tactic:
apply Nat.cast_dvd_cast
Proof state after:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
⊢ m ! ∣ (n - 1)!
Theorem: factorial_isUnit
Proof state before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
⊢ m ! ∣ (n - 1)!
Tactic:
apply Nat.factorial_dvd_factorial
Proof state after:
case h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
⊢ m ≤ n - 1
Theorem: factorial_isUnit
Proof state before:
case h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
⊢ m ≤ n - 1
Tactic:
exact Nat.le_sub_one_of_lt hmn
Proof state after:
no goals
Theorem: factorial_isUnit'
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑n !
m : ℕ
hmn : m ≤ n
⊢ IsUnit ↑m !
Tactic:
apply isUnit_of_dvd_unit _ hn_fac
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑n !
m : ℕ
hmn : m ≤ n
⊢ ↑m ! ∣ ↑n !
Theorem: factorial_isUnit'
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑n !
m : ℕ
hmn : m ≤ n
⊢ ↑m ! ∣ ↑n !
Tactic:
apply Nat.cast_dvd_cast
Proof state after:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑n !
m : ℕ
hmn : m ≤ n
⊢ m ! ∣ n !
Theorem: factorial_isUnit'
Proof state before:
case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑n !
m : ℕ
hmn : m ≤ n
⊢ m ! ∣ n !
Tactic:
apply Nat.factorial_dvd_factorial
Proof state after:
case h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑n !
m : ℕ
hmn : m ≤ n
⊢ m ≤ n
Theorem: factorial_isUnit'
Proof state before:
case h.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
hn_fac : IsUnit ↑n !
m : ℕ
hmn : m ≤ n
⊢ m ≤ n
Tactic:
exact hmn
Proof state after:
no goals
Theorem: Factorial.isUnit
Proof state before:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ IsUnit ↑n !
Tactic:
rw [← map_natCast (algebraMap ℚ A)]
Proof state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ IsUnit ((algebraMap ℚ A) ↑n !)
Theorem: Factorial.isUnit
Proof state before:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ IsUnit ((algebraMap ℚ A) ↑n !)
Tactic:
apply IsUnit.map
Proof state after:
case h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ IsUnit ↑n !
Theorem: Factorial.isUnit
Proof state before:
case h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ IsUnit ↑n !
Tactic:
rw [isUnit_iff_ne_zero]
Proof state after:
case h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑n ! ≠ 0
Theorem: Factorial.isUnit
Proof state before:
case h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑n ! ≠ 0
Tactic:
simp only [ne_eq, Nat.cast_eq_zero]
Proof state after:
case h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ¬n ! = 0
Theorem: Factorial.isUnit
Proof state before:
case h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ¬n ! = 0
Tactic:
exact Nat.factorial_ne_zero n
Proof state after:
no goals
Theorem: Ring.inverse_pow_mul_eq_iff_eq_mul
Proof state before:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b c : M₀
ha : IsUnit a
k : ℕ
⊢ inverse a ^ k * b = c ↔ b = a ^ k * c
Tactic:
rw [Ring.inverse_pow, Ring.inverse_mul_eq_iff_eq_mul _ _ _ (IsUnit.pow _ ha)]
Proof state after:
no goals
Theorem: Ideal.mem_pow_eq_zero
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = 0
hmn : n ≤ m
x : A
hx : x ∈ I
⊢ x ^ m = 0
Tactic:
have hxn : x ^ n = 0 := by
  rw [Ideal.zero_eq_bot] at hnI
  rw [← Ideal.mem_bot, ← hnI]
  exact Ideal.pow_mem_pow hx n
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = 0
hmn : n ≤ m
x : A
hx : x ∈ I
hxn : x ^ n = 0
⊢ x ^ m = 0
Theorem: Ideal.mem_pow_eq_zero
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = 0
hmn : n ≤ m
x : A
hx : x ∈ I
hxn : x ^ n = 0
⊢ x ^ m = 0
Tactic:
obtain ⟨c, hc⟩ := Nat.exists_eq_add_of_le hmn
Proof state after:
case intro
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = 0
hmn : n ≤ m
x : A
hx : x ∈ I
hxn : x ^ n = 0
c : ℕ
hc : m = n + c
⊢ x ^ m = 0
Theorem: Ideal.mem_pow_eq_zero
Proof state before:
case intro
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = 0
hmn : n ≤ m
x : A
hx : x ∈ I
hxn : x ^ n = 0
c : ℕ
hc : m = n + c
⊢ x ^ m = 0
Tactic:
rw [hc, pow_add, hxn, MulZeroClass.zero_mul]
Proof state after:
no goals
Theorem: Ideal.mem_pow_eq_zero
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = 0
hmn : n ≤ m
x : A
hx : x ∈ I
⊢ x ^ n = 0
Tactic:
rw [Ideal.zero_eq_bot] at hnI
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = ⊥
hmn : n ≤ m
x : A
hx : x ∈ I
⊢ x ^ n = 0
Theorem: Ideal.mem_pow_eq_zero
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = ⊥
hmn : n ≤ m
x : A
hx : x ∈ I
⊢ x ^ n = 0
Tactic:
rw [← Ideal.mem_bot, ← hnI]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = ⊥
hmn : n ≤ m
x : A
hx : x ∈ I
⊢ x ^ n ∈ I ^ n
Theorem: Ideal.mem_pow_eq_zero
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n m : ℕ
hnI : I ^ n = ⊥
hmn : n ≤ m
x : A
hx : x ∈ I
⊢ x ^ n ∈ I ^ n
Tactic:
exact Ideal.pow_mem_pow hx n
Proof state after:
no goals
Theorem: Algebra.TensorProduct.coe_map_id₁
Proof state before:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
S' : Type u_3
inst✝⁵ : Semiring S
inst✝⁴ : Semiring S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
φ : S →ₐ[R] S'
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ⇑(map (AlgHom.id R A) φ) = ⇑(LinearMap.lTensor A φ.toLinearMap)
Tactic:
rfl
Proof state after:
no goals
Theorem: Algebra.TensorProduct.coe_map_id₂
Proof state before:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
S' : Type u_3
inst✝⁵ : Semiring S
inst✝⁴ : Semiring S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
φ : S →ₐ[R] S'
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ⇑(map φ (AlgHom.id R A)) = ⇑(LinearMap.rTensor A φ.toLinearMap)
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPolynomial.coeff_baseChange_apply
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
m : σ →₀ ℕ
φ : S →ₐ[R] S'
f : MvPolynomial σ S
⊢ coeff m ((baseChange φ) f) = φ (coeff m f)
Tactic:
rw [baseChange, AlgHom.coe_mk, coe_eval₂RingHom]
Proof state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
m : σ →₀ ℕ
φ : S →ₐ[R] S'
f : MvPolynomial σ S
⊢ coeff m (eval₂ (C.comp ↑φ) X f) = φ (coeff m f)
Theorem: MvPolynomial.coeff_baseChange_apply
Proof state before:
case h_C
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
r : S
m : σ →₀ ℕ
⊢ coeff m (eval₂ (C.comp ↑φ) X (C r)) = φ (coeff m (C r))
Tactic:
simp only [eval₂_C, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, coeff_C]
Proof state after:
case h_C
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
r : S
m : σ →₀ ℕ
⊢ (if 0 = m then φ r else 0) = φ (if 0 = m then r else 0)
Theorem: MvPolynomial.coeff_baseChange_apply
Proof state before:
case h_C
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
r : S
m : σ →₀ ℕ
⊢ (if 0 = m then φ r else 0) = φ (if 0 = m then r else 0)
Tactic:
split_ifs
Proof state after:
case pos
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
r : S
m : σ →₀ ℕ
h✝ : 0 = m
⊢ φ r = φ r

case neg
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
r : S
m : σ →₀ ℕ
h✝ : ¬0 = m
⊢ 0 = φ 0
Theorem: MvPolynomial.coeff_baseChange_apply
Proof state before:
case pos
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
r : S
m : σ →₀ ℕ
h✝ : 0 = m
⊢ φ r = φ r
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPolynomial.coeff_baseChange_apply
Proof state before:
case neg
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
r : S
m : σ →₀ ℕ
h✝ : ¬0 = m
⊢ 0 = φ 0
Tactic:
rw [map_zero]
Proof state after:
no goals
Theorem: MvPolynomial.coeff_baseChange_apply
Proof state before:
case h_add
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
f g : MvPolynomial σ S
hf : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X f) = φ (coeff m f)
hg : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X g) = φ (coeff m g)
m : σ →₀ ℕ
⊢ coeff m (eval₂ (C.comp ↑φ) X (f + g)) = φ (coeff m (f + g))
Tactic:
simp only [eval₂_add, coeff_add, hf, hg, map_add]
Proof state after:
no goals
Theorem: MvPolynomial.coeff_baseChange_apply
Proof state before:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
⊢ coeff m (eval₂ (C.comp ↑φ) X (p * X s)) = φ (coeff m (p * X s))
Tactic:
simp only [eval₂_mul, eval₂_X, coeff_mul, map_sum, _root_.map_mul]
Proof state after:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
⊢ ∑ x ∈ Finset.antidiagonal m, coeff x.1 (eval₂ (C.comp ↑φ) X p) * coeff x.2 (X s) =
    ∑ x ∈ Finset.antidiagonal m, φ (coeff x.1 p) * φ (coeff x.2 (X s))
Theorem: MvPolynomial.coeff_baseChange_apply
Proof state before:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
⊢ ∑ x ∈ Finset.antidiagonal m, coeff x.1 (eval₂ (C.comp ↑φ) X p) * coeff x.2 (X s) =
    ∑ x ∈ Finset.antidiagonal m, φ (coeff x.1 p) * φ (coeff x.2 (X s))
Tactic:
apply Finset.sum_congr rfl
Proof state after:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
⊢ ∀ x ∈ Finset.antidiagonal m,
    coeff x.1 (eval₂ (C.comp ↑φ) X p) * coeff x.2 (X s) = φ (coeff x.1 p) * φ (coeff x.2 (X s))