ι : Type u_1
R : Type ?u.136196
M : Type u_2
A : Type ?u.136202
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ AddMonoidAlgebra.toDirectSum (toAddMonoidAlgebra (f * g)) =
    AddMonoidAlgebra.toDirectSum (toAddMonoidAlgebra f * toAddMonoidAlgebra g)

case inj
ι : Type u_1
R : Type ?u.136196
M : Type u_2
A : Type ?u.136202
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ Function.Injective AddMonoidAlgebra.toDirectSum
ι : Type u_1
R : Type ?u.136196
M : Type u_2
A : Type ?u.136202
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ toAddMonoidAlgebra (f * g) = toAddMonoidAlgebra f * toAddMonoidAlgebra g
apply_fun AddMonoidAlgebra.toDirectSum
no goals
ι : Type u_1
R : Type ?u.136196
M : Type u_2
A : Type ?u.136202
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ AddMonoidAlgebra.toDirectSum (toAddMonoidAlgebra (f * g)) =
    AddMonoidAlgebra.toDirectSum (toAddMonoidAlgebra f * toAddMonoidAlgebra g)
simp
case inj.a
ι : Type u_1
R : Type ?u.136196
M : Type u_2
A : Type ?u.136202
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ Function.LeftInverse ?inj.g AddMonoidAlgebra.toDirectSum

case inj.g
ι : Type u_1
R : Type ?u.136196
M : Type u_2
A : Type ?u.136202
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (⨁ (x : ι), M) → AddMonoidAlgebra M ι
case inj
ι : Type u_1
R : Type ?u.136196
M : Type u_2
A : Type ?u.136202
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ Function.Injective AddMonoidAlgebra.toDirectSum
apply Function.LeftInverse.injective
no goals
case inj.a
ι : Type u_1
R : Type ?u.136196
M : Type u_2
A : Type ?u.136202
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ Function.LeftInverse ?inj.g AddMonoidAlgebra.toDirectSum

case inj.g
ι : Type u_1
R : Type ?u.136196
M : Type u_2
A : Type ?u.136202
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (⨁ (x : ι), M) → AddMonoidAlgebra M ι
apply AddMonoidAlgebra.toDirectSum_toAddMonoidAlgebra