intCast_cast — Mathlib

English

For s in SignType and odd n, s^n = s in any additive group with one.

Русский

Для s в SignType и нечетного n верно s^n = s в любой группе с единицей.

LaTeX

$$$\forall s\in SignType,\; \text{Odd}(n) \Rightarrow s^n = s$$$

Lean4

/-- Casting `SignType → ℤ → α` is the same as casting directly `SignType → α`. -/
@[simp, norm_cast]
theorem intCast_cast {α : Type*} [AddGroupWithOne α] (s : SignType) : ((s : ℤ) : α) = s :=
  map_cast' _ Int.cast_one Int.cast_zero (@Int.cast_one α _ ▸ Int.cast_neg 1) _

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