Discrete rational probabilistic distribution to multiset

Stream: mathlib4

[Martin Dvořák]

Do we have a conversion of discrete rational probabilistic distributions to multisets?

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Rat.Basic
open scoped BigOperators

def distributionToMultiset {D : Type} [Nonempty D] [Fintype D] [DecidableEq D]
    {x : D → ℚ} (x_is_distribution : 0 ≤ x ∧ ∑ i, x i = 1) : Multiset D :=
  sorry

[Martin Dvořák]

Lemme break the problem into two parts. First, do we have a function for converting a list of rationals to a common denominator? Ideally, I would like something that transforms [1/3, 1/4, 1/4, 1/6] into [4, 3, 3, 2].

[Ruben Van de Velde]

field_simp must do something like that

[Martin Dvořák]

Do we have it as a function tho? I need a conversion function that comes with some Mathlib-friendly API.