M : Type u_2
ι : Type ?u.7453
R : Type u_1
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
m : M
a : AddMonoidAlgebra R M
⊢ (∃ b, a = Finsupp.single m b) ↔ a ∈ LinearMap.range (Finsupp.lsingle m)
M : Type u_2
ι : Type ?u.7453
R : Type u_1
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
m : M
a : AddMonoidAlgebra R M
⊢ a ∈ grade R m ↔ a ∈ LinearMap.range (Finsupp.lsingle m)
rw [mem_grade_iff, Finsupp.support_subset_singleton']
case h
M : Type u_2
ι : Type ?u.7453
R : Type u_1
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
m : M
a : AddMonoidAlgebra R M
⊢ ∀ (a_1 : R), a = Finsupp.single m a_1 ↔ ↑(Finsupp.lsingle m) a_1 = a
M : Type u_2
ι : Type ?u.7453
R : Type u_1
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
m : M
a : AddMonoidAlgebra R M
⊢ (∃ b, a = Finsupp.single m b) ↔ a ∈ LinearMap.range (Finsupp.lsingle m)
apply exists_congr
case h
M : Type u_2
ι : Type ?u.7453
R : Type u_1
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
m : M
a : AddMonoidAlgebra R M
r : R
⊢ a = Finsupp.single m r ↔ ↑(Finsupp.lsingle m) r = a
case h
M : Type u_2
ι : Type ?u.7453
R : Type u_1
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
m : M
a : AddMonoidAlgebra R M
⊢ ∀ (a_1 : R), a = Finsupp.single m a_1 ↔ ↑(Finsupp.lsingle m) a_1 = a
intro r
no goals
case h
M : Type u_2
ι : Type ?u.7453
R : Type u_1
inst✝¹ : DecidableEq M
inst✝ : CommSemiring R
m : M
a : AddMonoidAlgebra R M
r : R
⊢ a = Finsupp.single m r ↔ ↑(Finsupp.lsingle m) r = a
constructor <;> exact Eq.symm