English
FreeAbelianGroup is given a commutative applicative structure; the applicative product commutes in its tensor-like operation.
Русский
Свободная абелева группа снабжена коммутативной аппликативной структурой; произведение аппликативности коммутирует.
LaTeX
$$$ \text{CommApplicative}(\text{FreeAbelianGroup})$$$
Lean4
instance : CommApplicative FreeAbelianGroup.{u} where
commutative_prod x
y := by
refine FreeAbelianGroup.induction_on' x ?_ ?_ ?_ ?_
· rw [FreeAbelianGroup.map_zero, zero_seq, seq_zero]
· intro p
rw [map_pure, pure_seq]
exact
FreeAbelianGroup.induction_on' y (by rw [FreeAbelianGroup.map_zero, FreeAbelianGroup.map_zero, zero_seq])
(fun q ↦ by rw [map_pure, map_pure, pure_seq, map_pure])
(fun q ih ↦ by rw [FreeAbelianGroup.map_neg, FreeAbelianGroup.map_neg, neg_seq, ih]) fun y₁ y₂ ih1 ih2 ↦ by
rw [FreeAbelianGroup.map_add, FreeAbelianGroup.map_add, add_seq, ih1, ih2]
· intro p ih
rw [FreeAbelianGroup.map_neg, neg_seq, seq_neg, ih]
· intro x₁ x₂ ih1 ih2
rw [FreeAbelianGroup.map_add, add_seq, seq_add, ih1, ih2]
