natCast_eq_zero

Mathlib.Data.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.natCast_eq_zero

English

For any a,n with n > 0, (a : Fin n) = 0 iff n divides a: n | a.

Русский

Для любых a,n (n > 0) выполняется: (a : Fin n) = 0 тогда и только тогда, когда n делит a: n | a.

LaTeX

$$$\\forall {a,n} \\in \\mathbb{N}, 0 < n \\Rightarrow (a : \\mathrm{Fin}(n)) = 0 \\iff n \\mid a$$$

Lean4

@[simp]
theorem natCast_eq_zero {a n : ℕ} [NeZero n] : (a : Fin n) = 0 ↔ n ∣ a := by simp [Fin.ext_iff, Nat.dvd_iff_mod_eq_zero]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru