cast_neg — Mathlib

English

Casting distributes over negation: (cast (-a : ZMod n) : R) = -(cast a).

Русский

Приведение сохраняет отрицание: cast(-a) = -cast(a).

LaTeX

$$$\\\\forall {n : \\\\mathbb{N}} {R : Type*} [Ring R] {m : \\\\mathbb{N}} [CharP R m] (h : m \\\\mid n) (a : ZMod n), \\\\operatorname{cast} (-a) = -(\\\\operatorname{cast} a)$$$

Lean4

@[simp]
theorem cast_neg (h : m ∣ n) (a : ZMod n) : (cast (-a : ZMod n) : R) = -(cast a) :=
  (castHom h R).map_neg a

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