English
For v : ι → M and w : ι → R, piEquiv v evaluated at w equals the finite sum ∑_i w_i v_i.
Русский
Для v : ι → M и w : ι → R, применение piEquiv к (v,w) равно конечной сумме ∑_i w_i v_i.
LaTeX
$$piEquiv_apply_apply (ι R M) v w = ∑ i, w i • v i$$
Lean4
instance : CommSemiring (SymmetricAlgebra R M) where
mul_comm a
b := by
change Commute a b
induction b using SymmetricAlgebra.induction with
| algebraMap r => exact Algebra.commute_algebraMap_right _ _
| ι x =>
induction a using SymmetricAlgebra.induction with
| algebraMap r => exact Algebra.commute_algebraMap_left _ _
| ι y => simp [commute_iff_eq, ι, ← map_mul, RingQuot.mkAlgHom_rel _ (SymRel.mul_comm x y)]
| mul a b ha hb => exact ha.mul_left hb
| add a b ha hb => exact ha.add_left hb
| mul b c hb hc => exact hb.mul_right hc
| add b c hb hc => exact hb.add_right hc
