star_ofNat

Mathlib.Algebra.Star.Basic

URI: https://scilib.ai/kg/mathlib#star_ofNat

English

If n ≥ 2, star(ofNat(n)) = ofNat(n).

Русский

Если n ≥ 2, то star(ofNat(n)) = ofNat(n).

LaTeX

$$$$ (n : R)^{*} = n \quad (n \ge 2). $$$$

Lean4

@[simp]
theorem star_ofNat [NonAssocSemiring R] [StarRing R] (n : ℕ) [n.AtLeastTwo] : star (ofNat(n) : R) = ofNat(n) :=
  star_natCast _

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

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

Разделы

Аффилиация

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