Theorem: DirectSum.decomposeAlgEquiv_coe (DividedPowers/ForMathlib/GradedRingQuot.lean)

State before:
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
a : A
⊢ (decomposeAlgEquiv 𝒜) a = (decompose 𝒜) a
Tactic:
rfl
State after:
no goals