mk_natCast — Mathlib

English

For any nonzero natural number n, mk(n : S) = 0 in the Archimedean setting.

Русский

Для любого ненулевого натурального числа n выполняется mk(n : S) = 0 в рамках Архимедового контекста.

LaTeX

$$$\forall n \in \mathbb{N},\ n \neq 0 \Rightarrow \operatorname{mk}(n : S) = 0.$$$

Lean4

@[simp]
theorem mk_natCast {n : ℕ} (h : n ≠ 0) : mk (n : S) = 0 :=
  by
  rw [← Int.cast_natCast]
  exact mk_intCast (mod_cast h)

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