Nondependent sigma to pair

Stream: new members

[Horatiu Cheval]

Is there defined in Lean a standard way of converting non-dependent Sigma types to plain product types?
Something like this:

  def sigma_to_pair {α β : Type} : (Σ _ : α, β) → α × β
  | (sigma.mk a b) := (a, b)

[Eric Wieser]

docs#equiv.sigma_equiv_prod

[Horatiu Cheval]

Perfect, thanks