Results are reported for the B_s⁰ → μ⁺μ^- branching fraction and effective lifetime and from a search for the decay B⁰ → μ⁺μ^-. The analysis uses a data sample of proton-proton collisions accumulated by the CMS experiment in 2011, 2012, and 2016, with center-of-mass energies (integrated luminosities) of 7 TeV (5 fb^-1), 8 TeV (20 fb^-1), and 13 TeV (36 fb^-1). The branching fractions are determined by measuring event yields relative to B⁺ → J/ψK⁺ decays (with J/ψ → μ⁺μ^-), which results in the reduction of many of the systematic uncertainties. The decay B_s⁰ → μ⁺μ^- is observed with a significance of 5.6 standard deviations. The branching fraction is measured to be B(B_s⁰ → μ⁺μ^-) = [2.9 ± 0.7(exp) ± 0.2(frag)] × 10^-9, where the first uncertainty combines the experimental statistical and systematic contributions, and the second is due to the uncertainty in the ratio of the B_s⁰ and the B⁺ fragmentation functions. No significant excess is observed for the decay B⁰ → μ⁺μ^-, and an upper limit of B(B⁰ → μ⁺μ^-) < 3.6 × 10^-10 is obtained at 95% confidence level. The B_s⁰ → μ⁺μ^- effective lifetime is measured to be τ_μ⁺μ- = 1.70_-0.44^+0.61 ps. These results are consistent with standard model predictions. [Figure not available: see fulltext.].