intCast_def' — Mathlib

English

For n with NeZero n, Fin(n) has AddMonoidWithOne structure with natCast from Nat.

Русский

Для n, не равного нулю, Fin(n) имеет структуру AddMonoidWithOne с отображением natCast из натуральных чисел.

LaTeX

$$$\\forall n\\, \\operatorname{AddMonoidWithOne}(\\mathrm{Fin}(n))\\, (n\\neq 0)$$$

Lean4

/-- Variant of `Fin.intCast_def` with `Nat.cast` on the RHS. -/
theorem intCast_def' {n : Nat} [NeZero n] (x : Int) : (x : Fin n) = if 0 ≤ x then ↑x.natAbs else -↑x.natAbs :=
  Fin.intCast_def _

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