English
If f is irreducible in K[X], then AdjoinRoot f carries a field structure.
Русский
Если f ирредуцируемый в K[X], то AdjoinRoot f имеет структуру поля.
LaTeX
$$Field(AdjoinRoot f) holds when Irreducible f$$
Lean4
/-- If `R` is a field and `f` is irreducible, then `AdjoinRoot f` is a field -/
@[stacks 09FX "first part, see also 09FI"]
noncomputable instance instField [Fact (Irreducible f)] : Field (AdjoinRoot f)
where
__ := instCommRing _
__ := instGroupWithZero
nnqsmul := (· • ·)
qsmul := (· • ·)
nnratCast_def q := by rw [← map_natCast (of f), ← map_natCast (of f), ← map_div₀, ← NNRat.cast_def]; rfl
ratCast_def q := by rw [← map_natCast (of f), ← map_intCast (of f), ← map_div₀, ← Rat.cast_def]; rfl
nnqsmul_def q
x :=
AdjoinRoot.induction_on f (C := fun y ↦ q • y = (of f) q * y) x fun p ↦ by
simp only [smul_mk, of, RingHom.comp_apply, ← (mk f).map_mul, Polynomial.nnqsmul_eq_C_mul]
qsmul_def q
x :=
-- Porting note: I gave the explicit motive and changed `rw` to `simp`.
AdjoinRoot.induction_on f (C := fun y ↦ q • y = (of f) q * y) x fun p ↦ by
simp only [smul_mk, of, RingHom.comp_apply, ← (mk f).map_mul, Polynomial.qsmul_eq_C_mul]
