natCast_eq_one — Mathlib

English

In an IdemSemiring, if n ≠ 0, then the image of n under the natural casting equals 1: (n:α) = 1.

Русский

В IdemSemiring, если n ≠ 0, то образ n через натуральное включение равен 1: (n:α) = 1.

LaTeX

$$$ n \neq 0 \Rightarrow (n : \alpha) = 1 $$$

Lean4

theorem natCast_eq_one {n : ℕ} (nezero : n ≠ 0) : (n : α) = 1 :=
  by
  rw [← Nat.one_le_iff_ne_zero] at nezero
  induction n, nezero using Nat.le_induction with
  | base => exact Nat.cast_one
  | succ x _ hx => rw [Nat.cast_add, hx, Nat.cast_one, add_idem 1]

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