Let $k$ a commutative ring. Let $A$ be an $k$-algebra of finite presentation $A = k[\underline{X}] / \langle \underline{P} \rangle$ and $K / k$ free algebra of rank $r$.

There is a $k$-algebra $A \rtimes_k K$ representing the functeur from $k$-algebra to set given by $R \mapsto \text{Hom}_k(A,R \otimes K)$. I think this is call Weil-restriction (?).

I think we have : $$ \Omega_{A \rtimes K}^\star \simeq \Omega_{A / k}^\star \otimes_A ((A \rtimes_k K) \otimes K) $$

Comments : (i) the structure of $A$-algebra of $(A \rtimes_k K) \otimes K$ is given by the morphism $\iota : A \to A \rtimes_k K \otimes_k K$ corresponding to $\text{Id} : A \rtimes K \to A \rtimes K$. (ii) $$ \Omega_{A / k}^\star \otimes_A ((A \rtimes_k K) \otimes_k K) $$ is a $(A \rtimes_k K) \otimes K$-module and we view as an $(A \rtimes K)$-module via the restriction $A\rtimes K \to A \rtimes K \otimes K$ given by $x \mapsto x \otimes 1$.

Question : Do you know a reference for this result ?

Edit : dual !