getElem?_getD_replicate_default_eq

Mathlib.Data.List.GetD

URI: https://scilib.ai/kg/mathlib#List.getElem?_getD_replicate_default_eq

English

For any replicate list, the n-th getD with default equals the element being replicated.

Русский

Для повторяющегося списка n-й getElem?_getD с дефолтом возвращает скопированное значение.

LaTeX

$$$$ (\\mathrm{replicate}\\ r\\ d)[n]?.getD d = d $$$$

Lean4

@[simp]
theorem getElem?_getD_replicate_default_eq (r n : ℕ) : (replicate r d)[n]?.getD d = d := by grind

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

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

Разделы

Аффилиация

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