randFin

Mathlib.Control.Random

URI: https://scilib.ai/kg/mathlib#Random.randFin

Lean4

/-- Generate a random `Fin`. -/
def randFin {n : Nat} [NeZero n] [RandomGen g] : RandGT g m (Fin n) := fun ⟨g⟩ ↦
  pure <| randNat g 0 (n - 1) |>.map (Fin.ofNat n) ULift.up

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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