restrictDvd_surjective — Mathlib

English

If p divides q and q ≠ 0, then restrictDvd hpq is surjective.

Русский

Если p делится на q и q ≠ 0, то restrictDvd hpq сюръективен.

LaTeX

$$$\\operatorname{Surjective}(\\mathrm{restrictDvd}\\ hpq)$$$

Lean4

theorem restrictDvd_surjective (hpq : p ∣ q) (hq : q ≠ 0) : Function.Surjective (restrictDvd hpq) := by
  classical
  haveI := Fact.mk <| splits_of_splits_of_dvd (algebraMap F q.SplittingField) hq (SplittingField.splits q) hpq
  simpa only [restrictDvd_def, dif_neg hq] using restrict_surjective _ _

Похожие утверждения