A random sample of size $n=100$ has a mean $\bar{x}=1023$ and a sample standard deviation $s=5.3$. Find a $95%$ confidence interval for the population mean.
I understand that the standardized sample mean will be of the form $\frac{\bar{x}-\mu}{s/\sqrt{n}}$, which because we are using an estimated standard error of the mean vs. the standard error of the mean would imply we use the t-statistic, right?