diff --git a/CHANGELOG.md b/CHANGELOG.md
index 54670738d570f38ba1cec56fc93ec6f4d7d1e900..50b92c5020a4789f55ef51bd21be69360e1d4df5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -103,6 +103,8 @@ and Tej Chajed. Thanks a lot to everyone involved!
 * Rename `laterN_plus` into `laterN_add`.
 * Remove `make_laterable` from atomic updates. This relies on Iris now having
   support for later credits (see below).
+* Add `Fractional` and `AsFractional` instances for `embed` such that the
+  embedding of something fractional is also fractional. (by Simon Friis Vindum).
 
 **Changes in `proofmode`:**
 
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 2303c1c3172aa0589a87cdba4a2eb919ee4e05cd..05917ee57d6eafc63eb15ae736fe84ac37511165 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -87,6 +87,14 @@ Section fractional.
     rewrite !assoc. f_equiv. by rewrite comm.
   Qed.
 
+  Global Instance fractional_embed `{!BiEmbed PROP PROP'} Φ :
+    Fractional Φ → Fractional (λ q, ⎡ Φ q ⎤ : PROP')%I.
+  Proof. intros ???. by rewrite fractional embed_sep. Qed.
+
+  Global Instance as_fractional_embed `{!BiEmbed PROP PROP'} P Φ q :
+    AsFractional P Φ q → AsFractional (⎡ P ⎤) (λ q, ⎡ Φ q ⎤)%I q.
+  Proof. split; [by rewrite ->!as_fractional | apply _]. Qed.
+
   Global Instance fractional_big_sepL {A} (l : list A) Ψ :
     (∀ k x, Fractional (Ψ k x)) →
     Fractional (PROP:=PROP) (λ q, [∗ list] k↦x ∈ l, Ψ k x q)%I.
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 638add08ebd83ffded99a1b0dc59f845467ea583..d7d70dce93dd295046fcd1294255408601e9d51b 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -1,5 +1,6 @@
+From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics monpred.
-From iris.base_logic.lib Require Import invariants.
+From iris.base_logic.lib Require Import invariants ghost_var.
 From iris.prelude Require Import options.
 
 Unset Mangle Names.
@@ -183,6 +184,7 @@ Section tests_iprop.
   Context {I : biIndex} `{!invGS_gen hlc Σ}.
 
   Local Notation monPred := (monPred I (iPropI Σ)).
+  Local Notation monPredI := (monPredI I (iPropI Σ)).
   Implicit Types P Q R : monPred.
   Implicit Types 𝓟 𝓠 𝓡 : iProp Σ.
 
@@ -210,4 +212,9 @@ Section tests_iprop.
     iPoseProof (own_update with "Hγ") as "H"; first done.
     by iMod "H".
   Qed.
+
+  Lemma test_embed_fractional `{!ghost_varG Σ A} γ q (a : A) :
+    ⎡ghost_var γ q a⎤ ⊢@{monPredI} ⎡ghost_var γ (q/2) a⎤ ∗ ⎡ghost_var γ (q/2) a⎤.
+  Proof. iIntros "[$ $]". Qed.
+
 End tests_iprop.