coe_zsmul — Mathlib

English

The sections form an additive commutative group under pointwise operations.

Русский

Секции образуют аддитивную коммутативную группу по точечным операциям.

LaTeX

$$$\text{instAddCommGroup}$: $C_\s^n(I;F,V)$ is an AddCommGroup.$$

Lean4

@[simp]
theorem coe_zsmul (s : Cₛ^n⟮I; F, V⟯) (z : ℤ) : ⇑(z • s : Cₛ^n⟮I; F, V⟯) = z • ⇑s :=
  by
  rcases z with n | n
  · refine (coe_nsmul s n).trans ?_
    simp only [Int.ofNat_eq_coe, natCast_zsmul]
  · refine (congr_arg Neg.neg (coe_nsmul s (n + 1))).trans ?_
    simp only [negSucc_zsmul]

Похожие утверждения