English
The explicit formula for restrictDvd: it is equal to 1 if q = 0, otherwise it is the restrict map with a Splits witness provided by splits_of_splits_of_dvd.
Русский
Явное выражение restrictDvd: равно 1 при q = 0, иначе — ограничение p с доказательством распада через splits_of_splits_of_dvd.
LaTeX
$$$\\text{restrictDvd } hpq = \\begin{cases} 1, & \\text{if } q=0 \\\\ @\\restrict\\ F\\_\\ p\\ _ \\ _ ⟨splits\\_of\\_splits\\_of\\_dvd (algebraMap F q.SplittingField) \\ \\ _⟩, & \\text{otherwise} \\end{cases}$$$
Lean4
theorem restrictDvd_def [Decidable (q = 0)] (hpq : p ∣ q) :
restrictDvd hpq =
if hq : q = 0 then 1
else
@restrict F _ p _ _ _
⟨splits_of_splits_of_dvd (algebraMap F q.SplittingField) hq (SplittingField.splits q) hpq⟩ :=
by
unfold restrictDvd
congr
