Theorem: PolynomialMap.finsupp_polynomialMap_of_coeff (DividedPowers/PolynomialMap/Coeff.lean)

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
f : M →ₚ[R] N
⊢ Finsupp.polynomialMap b ((coeff ⇑b) f) = f
Tactic:
apply coeff_injective (DFunLike.coe b)
State after:
case hm
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
f : M →ₚ[R] N
⊢ Submodule.span R (Set.range ⇑b) = ⊤

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
f : M →ₚ[R] N
⊢ (coeff ⇑b) (Finsupp.polynomialMap b ((coeff ⇑b) f)) = (coeff ⇑b) f

State before:
case hm
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
f : M →ₚ[R] N
⊢ Submodule.span R (Set.range ⇑b) = ⊤
Tactic:
rw [_root_.eq_top_iff]
State after:
case hm
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
f : M →ₚ[R] N
⊢ ⊤ ≤ Submodule.span R (Set.range ⇑b)

State before:
case hm
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
f : M →ₚ[R] N
⊢ ⊤ ≤ Submodule.span R (Set.range ⇑b)
Tactic:
intro m _
State after:
case hm
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
f : M →ₚ[R] N
m : M
a✝ : m ∈ ⊤
⊢ m ∈ Submodule.span R (Set.range ⇑b)

State before:
case hm
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
f : M →ₚ[R] N
m : M
a✝ : m ∈ ⊤
⊢ m ∈ Submodule.span R (Set.range ⇑b)
Tactic:
apply Submodule.span_mono _ (Basis.mem_span_repr_support b m)
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
f : M →ₚ[R] N
m : M
a✝ : m ∈ ⊤
⊢ ⇑b '' ↑(b.repr m).support ⊆ Set.range ⇑b

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
f : M →ₚ[R] N
m : M
a✝ : m ∈ ⊤
⊢ ⇑b '' ↑(b.repr m).support ⊆ Set.range ⇑b
Tactic:
apply Set.image_subset_range
State after:
no goals

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
f : M →ₚ[R] N
⊢ (coeff ⇑b) (Finsupp.polynomialMap b ((coeff ⇑b) f)) = (coeff ⇑b) f
Tactic:
rw [coeff_of_finsupp_polynomialMap]
State after:
no goals