For a field $K\subset \mathbb{Q}(\zeta_p)$ $~$($\zeta_p$ a primitive pth root of unity, p a prime), it seems to be the case that the discriminant of $K$ is $p^{[K:\mathbb{Q}]-1}$ (according to Sage). How can I prove that/ is the proof implied by something written down somewhere?
I have a feeling this is somewhat deep so I ask it here; if it's insufficiently deep I'm happy to close it and ask elsewhere.