Skip to content

Commit

Permalink
chore(ring_theory/adjoin_root): modify field instance on `adjoin_ro…
Browse files Browse the repository at this point in the history
…ot` (#19119)

We copy the fields of `group_with_zero` instead of `field`.  This speeds up the already ported `adjoin_root/AdjoinRoot` pair.

[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234339.20.20FieldTheory.2ESplittingField)
  • Loading branch information
adomani committed May 28, 2023
1 parent f7ebde7 commit 5c4b3d4
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/ring_theory/adjoin_root.lean
Original file line number Diff line number Diff line change
Expand Up @@ -322,7 +322,7 @@ noncomputable instance field [fact (irreducible f)] : field (adjoin_root f) :=
qsmul_eq_mul' := λ a x, adjoin_root.induction_on _ x (λ p,
by { rw [smul_mk, of, ring_hom.comp_apply, ← (mk f).map_mul, polynomial.rat_smul_eq_C_mul] }),
..adjoin_root.comm_ring f,
..ideal.quotient.field (span {f} : ideal K[X]) }
..ideal.quotient.group_with_zero (span {f} : ideal K[X]) }

lemma coe_injective (h : degree f ≠ 0) : function.injective (coe : K → adjoin_root f) :=
have _ := adjoin_root.nontrivial f h, by exactI (of f).injective
Expand Down

0 comments on commit 5c4b3d4

Please sign in to comment.