Skip to content

Commit 2443f91

Browse files
artie2000pechersky
artie2000
authored and
pechersky
committed
feat(RingTheory/IsAdjoinRoot): add properties and constructors (leanprover-community#27373)
* Add facts about `IsAdjoinRoot`: root is primitive, root is algebraic/integral, extension dimension, isomorphism with `AdjoinRoot` * Redefine isomorphism constructors to use the isomorphism with `AdjoinRoot` * Add constructors for `IsAdjoinRoot` from primitive element
1 parent 41750d0 commit 2443f91

File tree

2 files changed

+203
-105
lines changed

2 files changed

+203
-105
lines changed

‎Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean‎

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -86,10 +86,16 @@ theorem adjoin_algebraic_toSubalgebra {S : Set E} (hS : ∀ x ∈ S, IsAlgebraic
8686
(Algebra.IsIntegral.adjoin fun x hx ↦ (hS x hx).isIntegral).inv_mem
8787

8888
theorem adjoin_simple_toSubalgebra_of_integral (hα : IsIntegral F α) :
89-
F⟮α⟯.toSubalgebra = Algebra.adjoin F {α} := by
90-
apply adjoin_algebraic_toSubalgebra
91-
rintro x (rfl : x = α)
92-
rwa [isAlgebraic_iff_isIntegral]
89+
F⟮α⟯.toSubalgebra = Algebra.adjoin F {α} :=
90+
adjoin_algebraic_toSubalgebra <| by simpa [isAlgebraic_iff_isIntegral]
91+
92+
lemma _root_.Algebra.adjoin_eq_top_of_intermediateField {S : Set E} (hS : ∀ x ∈ S, IsAlgebraic F x)
93+
(hS₂ : IntermediateField.adjoin F S = ⊤) : Algebra.adjoin F S = ⊤ := by
94+
simp [*, ← IntermediateField.adjoin_algebraic_toSubalgebra hS]
95+
96+
lemma _root_.Algebra.adjoin_eq_top_of_primitive_element {α : E} (hα : IsIntegral F α)
97+
(hα₂ : F⟮α⟯ = ⊤) : Algebra.adjoin F {α} = ⊤ :=
98+
Algebra.adjoin_eq_top_of_intermediateField (by simpa [isAlgebraic_iff_isIntegral]) hα₂
9399

94100
lemma finite_of_fg_of_isAlgebraic
95101
(h : IntermediateField.FG (⊤ : IntermediateField F E)) [Algebra.IsAlgebraic F E] :

‎Mathlib/RingTheory/IsAdjoinRoot.lean‎

Lines changed: 193 additions & 101 deletions
Original file line numberDiff line numberDiff line change
@@ -134,6 +134,22 @@ theorem aeval_root_self : aeval h.root f = 0 := by simp
134134

135135
@[deprecated (since := "2025-07-23")] alias aeval_root := aeval_root_self
136136

137+
theorem adjoin_root_eq_top : Algebra.adjoin R {h.root} = ⊤ := by
138+
rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top, aeval_root_eq_map]
139+
exact h.map_surjective
140+
141+
/-- Extensionality of the `IsAdjoinRoot` structure itself. See `IsAdjoinRootMonic.ext_elem`
142+
for extensionality of the ring elements. -/
143+
theorem ext_map (h' : IsAdjoinRoot S f) (eq : ∀ x, h.map x = h'.map x) : h = h' := by
144+
cases h; cases h'; congr
145+
exact AlgHom.ext eq
146+
147+
/-- Extensionality of the `IsAdjoinRoot` structure itself. See `IsAdjoinRootMonic.ext_elem`
148+
for extensionality of the ring elements. -/
149+
@[ext]
150+
theorem ext (h' : IsAdjoinRoot S f) (eq : h.root = h'.root) : h = h' :=
151+
h.ext_map h' (fun x => by rw [← h.aeval_root_eq_map, ← h'.aeval_root_eq_map, eq])
152+
137153
/-- Choose an arbitrary representative so that `h.map (h.repr x) = x`.
138154
139155
If `f` is monic, use `IsAdjoinRootMonic.modByMonicHom` for a unique choice of representative.
@@ -150,17 +166,118 @@ theorem repr_zero_mem_span : h.repr 0 ∈ Ideal.span ({f} : Set R[X]) := by simp
150166
theorem repr_add_sub_repr_add_repr_mem_span (x y : S) :
151167
h.repr (x + y) - (h.repr x + h.repr y) ∈ Ideal.span ({f} : Set R[X]) := by simp [← h.ker_map]
152168

153-
/-- Extensionality of the `IsAdjoinRoot` structure itself. See `IsAdjoinRootMonic.ext_elem`
154-
for extensionality of the ring elements. -/
155-
theorem ext_map (h' : IsAdjoinRoot S f) (eq : ∀ x, h.map x = h'.map x) : h = h' := by
156-
cases h; cases h'; congr
157-
exact AlgHom.ext eq
169+
section Equiv
158170

159-
/-- Extensionality of the `IsAdjoinRoot` structure itself. See `IsAdjoinRootMonic.ext_elem`
160-
for extensionality of the ring elements. -/
161-
@[ext]
162-
theorem ext (h' : IsAdjoinRoot S f) (eq : h.root = h'.root) : h = h' :=
163-
h.ext_map h' (fun x => by rw [← h.aeval_root_eq_map, ← h'.aeval_root_eq_map, eq])
171+
variable {T : Type*} [Ring T] [Algebra R T]
172+
173+
/-- Algebra isomorphism with `R[X]/(f)`. -/
174+
def adjoinRootAlgEquiv : AdjoinRoot f ≃ₐ[R] S :=
175+
(Ideal.quotientEquivAlgOfEq R h.ker_map.symm).trans <|
176+
Ideal.quotientKerAlgEquivOfSurjective h.map_surjective
177+
178+
@[simp]
179+
theorem adjoinRootAlgEquiv_apply_mk (g : R[X]) :
180+
h.adjoinRootAlgEquiv (AdjoinRoot.mk f g) = h.map g := rfl
181+
182+
theorem adjoinRootAlgEquiv_apply_eq_map (a : AdjoinRoot f) :
183+
h.adjoinRootAlgEquiv a = h.map (AdjoinRoot.mk_surjective a).choose := by
184+
rw (occs := [1]) [← (AdjoinRoot.mk_surjective a).choose_spec, adjoinRootAlgEquiv_apply_mk]
185+
186+
theorem adjoinRootAlgEquiv_symm_apply_eq_mk (a : S) :
187+
h.adjoinRootAlgEquiv.symm a = AdjoinRoot.mk f (h.repr a) := by
188+
rw (occs := [1]) [AlgEquiv.symm_apply_eq, ← h.map_repr a, adjoinRootAlgEquiv_apply_mk]
189+
190+
@[simp]
191+
theorem adjoinRootAlgEquiv_apply_root : h.adjoinRootAlgEquiv (AdjoinRoot.root f) = h.root := rfl
192+
193+
@[simp]
194+
theorem adjoinRootAlgEquiv_symm_apply_root : h.adjoinRootAlgEquiv.symm h.root = AdjoinRoot.root f :=
195+
(AlgEquiv.symm_apply_eq h.adjoinRootAlgEquiv).mpr rfl
196+
197+
variable (h' : IsAdjoinRoot T f)
198+
199+
/-- Adjoining a root gives a unique algebra up to isomorphism.
200+
201+
This is the converse of `IsAdjoinRoot.ofAlgEquiv`: this turns an `IsAdjoinRoot` into an
202+
`AlgEquiv`, and `IsAdjoinRoot.ofAlgEquiv` turns an `AlgEquiv` into an `IsAdjoinRoot`.
203+
-/
204+
def algEquiv : S ≃ₐ[R] T := h.adjoinRootAlgEquiv.symm.trans h'.adjoinRootAlgEquiv
205+
206+
@[deprecated (since := "2025-08-13")] noncomputable alias aequiv := algEquiv
207+
208+
theorem algEquiv_def : h.algEquiv h' = h.adjoinRootAlgEquiv.symm.trans h'.adjoinRootAlgEquiv := rfl
209+
210+
@[simp]
211+
theorem algEquiv_root : h.algEquiv h' h.root = h'.root := by simp [algEquiv_def]
212+
213+
@[deprecated (since := "2025-08-13")] alias aequiv_root := algEquiv_root
214+
215+
@[simp]
216+
theorem algEquiv_map : AlgHom.comp (h.algEquiv h') h.map = h'.map := by
217+
ext; simp
218+
219+
@[deprecated (since := "2025-08-13")] alias aequiv_map := algEquiv_map
220+
221+
@[simp]
222+
theorem algEquiv_apply_map (z : R[X]) : h.algEquiv h' (h.map z) = h'.map z := by
223+
rw [← h.algEquiv_map h']; simp [-algEquiv_map]
224+
225+
@[simp] theorem algEquiv_self : h.algEquiv h = AlgEquiv.refl := by ext; simp [algEquiv_def]
226+
227+
@[deprecated (since := "2025-08-13")] alias aequiv_self := algEquiv_self
228+
229+
@[simp] theorem algEquiv_symm : (h.algEquiv h').symm = h'.algEquiv h := rfl
230+
231+
@[deprecated (since := "2025-08-13")] alias aequiv_symm := algEquiv_symm
232+
233+
@[simp]
234+
theorem algEquiv_algEquiv {U : Type*} [Ring U] [Algebra R U] (h'' : IsAdjoinRoot U f) (x) :
235+
(h'.algEquiv h'') (h.algEquiv h' x) = h.algEquiv h'' x := by simp [algEquiv_def]
236+
237+
@[deprecated (since := "2025-08-13")] alias aequiv_aequiv := algEquiv_algEquiv
238+
239+
@[simp]
240+
theorem algEquiv_trans {U : Type*} [Ring U] [Algebra R U] (h'' : IsAdjoinRoot U f) :
241+
(h.algEquiv h').trans (h'.algEquiv h'') = h.algEquiv h'' := by ext; simp
242+
243+
@[deprecated (since := "2025-08-13")] alias aequiv_trans := algEquiv_trans
244+
245+
/-- Transfer `IsAdjoinRoot` across an algebra isomorphism.
246+
247+
This is the converse of `IsAdjoinRoot.algEquiv`: this turns an `AlgEquiv` into an `IsAdjoinRoot`,
248+
and `IsAdjoinRoot.algEquiv` turns an `IsAdjoinRoot` into an `AlgEquiv`.
249+
-/
250+
@[simps! map_apply]
251+
def ofAlgEquiv (e : S ≃ₐ[R] T) : IsAdjoinRoot T f where
252+
map := (e : S →ₐ[R] T).comp h.map
253+
map_surjective := e.surjective.comp h.map_surjective
254+
ker_map := by ext; simp [Ideal.mem_span_singleton]
255+
256+
@[deprecated (since := "2025-08-13")] alias ofEquiv := ofAlgEquiv
257+
258+
@[simp] theorem ofAlgEquiv_root (e : S ≃ₐ[R] T) : (h.ofAlgEquiv e).root = e h.root := rfl
259+
260+
@[deprecated (since := "2025-08-13")] alias ofEquiv_root := ofAlgEquiv_root
261+
262+
@[simp]
263+
theorem algEquiv_ofAlgEquiv {U : Type*} [Ring U] [Algebra R U] (e : T ≃ₐ[R] U) :
264+
h.algEquiv (h'.ofAlgEquiv e) = (h.algEquiv h').trans e := by
265+
ext a
266+
simp [algEquiv_def, AlgEquiv.trans_apply, adjoinRootAlgEquiv_apply_eq_map, ofAlgEquiv_map_apply]
267+
268+
@[deprecated (since := "2025-08-13")] alias aequiv_ofEquiv := algEquiv_ofAlgEquiv
269+
270+
@[simp]
271+
theorem ofAlgEquiv_algEquiv {U : Type*} [Ring U] [Algebra R U] (h'' : IsAdjoinRoot U f)
272+
(e : S ≃ₐ[R] T) : (h.ofAlgEquiv e).algEquiv h'' = e.symm.trans (h.algEquiv h'') := by
273+
ext a
274+
simp_rw [algEquiv_def, AlgEquiv.trans_apply, EmbeddingLike.apply_eq_iff_eq,
275+
AlgEquiv.symm_apply_eq, adjoinRootAlgEquiv_apply_eq_map, ofAlgEquiv_map_apply,
276+
← adjoinRootAlgEquiv_apply_eq_map, AlgEquiv.apply_symm_apply]
277+
278+
@[deprecated (since := "2025-08-13")] alias ofEquiv_aequiv := ofAlgEquiv_algEquiv
279+
280+
end Equiv
164281

165282
section lift
166283

@@ -242,6 +359,8 @@ theorem eq_liftHom (g : S →ₐ[R] T) (hroot : g h.root = x) : g = h.liftHom x
242359

243360
end lift
244361

362+
theorem isAlgebraic_root (hf : f ≠ 0) : IsAlgebraic R h.root := ⟨f, by simp [hf]⟩
363+
245364
end IsAdjoinRoot
246365

247366
namespace AdjoinRoot
@@ -283,6 +402,10 @@ theorem isAdjoinRootMonic_root_eq_root (hf : Monic f) :
283402

284403
end AdjoinRoot
285404

405+
/-- If `S` is `R`-isomorphic to `R[X]/(f)`, then `S` is given by adjoining a root of `f`. -/
406+
abbrev IsAdjoinRoot.ofAdjoinRootEquiv (e : AdjoinRoot f ≃ₐ[R] S) : IsAdjoinRoot S f :=
407+
ofAlgEquiv (AdjoinRoot.isAdjoinRoot f) e
408+
286409
namespace IsAdjoinRootMonic
287410

288411
variable (h : IsAdjoinRootMonic S f)
@@ -399,6 +522,13 @@ theorem basis_repr (x : S) (i : Fin (natDegree f)) :
399522
theorem basis_one (hdeg : 1 < natDegree f) : h.basis ⟨1, hdeg⟩ = h.root := by
400523
rw [h.basis_apply, Fin.val_mk, pow_one]
401524

525+
include h in
526+
theorem finite : Module.Finite R S := (powerBasis h).finite
527+
528+
include h in
529+
theorem finrank [StrongRankCondition R] : Module.finrank R S = f.natDegree :=
530+
(powerBasis h).finrank
531+
402532
/-- `IsAdjoinRootMonic.liftPolyₗ` lifts a linear map on polynomials to a linear map on `S`. -/
403533
@[simps!]
404534
def liftPolyₗ {T : Type*} [AddCommGroup T] [Module R T] (g : R[X] →ₗ[R] T) : S →ₗ[R] T :=
@@ -500,114 +630,50 @@ theorem lift_self : h.lift (algebraMap R S) h.root h.aeval_root_self = RingHom.i
500630

501631
end lift
502632

503-
section Equiv
633+
section mkOfAdjoinEqTop
504634

505-
variable {T : Type*} [CommRing T] [Algebra R T]
635+
variable [IsDomain R] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R]
636+
{α : S} {hα : IsIntegral R α} {hα₂ : Algebra.adjoin R {α} = ⊤}
506637

507-
/-- Adjoining a root gives a unique ring up to algebra isomorphism.
638+
variable (hα hα₂) in
639+
/-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
640+
def mkOfAdjoinEqTop : IsAdjoinRoot S (minpoly R α) where
641+
map := aeval α
642+
map_surjective := by
643+
rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← Algebra.adjoin_singleton_eq_range_aeval,
644+
hα₂, Algebra.coe_top]
645+
ker_map := by
646+
ext
647+
simpa [Ideal.mem_span_singleton] using minpoly.isIntegrallyClosed_dvd_iff hα _
508648

509-
This is the converse of `IsAdjoinRoot.ofAlgEquiv`: this turns an `IsAdjoinRoot` into an
510-
`AlgEquiv`, and `IsAdjoinRoot.ofAlgEquiv` turns an `AlgEquiv` into an `IsAdjoinRoot`.
511-
-/
512-
def algEquiv (h' : IsAdjoinRoot T f) : S ≃ₐ[R] T :=
513-
{ h.liftHom h'.root h'.aeval_root_self with
514-
toFun := h.liftHom h'.root h'.aeval_root_self
515-
invFun := h'.liftHom h.root h.aeval_root_self
516-
left_inv x := by rw [← h.map_repr x]; simp [- map_repr]
517-
right_inv x := by rw [← h'.map_repr x]; simp [- map_repr] }
518-
519-
@[deprecated (since := "2025-08-13")] noncomputable alias aequiv := algEquiv
520-
521-
@[simp]
522-
theorem algEquiv_map (h' : IsAdjoinRoot T f) (z : R[X]) : h.algEquiv h' (h.map z) = h'.map z := by
523-
rw [algEquiv, AlgEquiv.coe_mk, Equiv.coe_fn_mk, liftHom_map, aeval_root_eq_map]
524-
525-
@[deprecated (since := "2025-08-13")] alias aequiv_map := algEquiv_map
526-
527-
@[simp]
528-
theorem algEquiv_root (h' : IsAdjoinRoot T f) : h.algEquiv h' h.root = h'.root := by
529-
rw [algEquiv, AlgEquiv.coe_mk, Equiv.coe_fn_mk, liftHom_root]
530-
531-
@[deprecated (since := "2025-08-13")] alias aequiv_root := algEquiv_root
649+
variable (hα hα₂) in
650+
/-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
651+
abbrev _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop : IsAdjoinRootMonic S (minpoly R α) where
652+
__ := IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂
653+
monic := minpoly.monic hα
532654

533655
@[simp]
534-
theorem algEquiv_self : h.algEquiv h = AlgEquiv.refl := by
535-
ext a; exact h.lift_self_apply a
656+
theorem mkOfAdjoinEqTop_root : (IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂).root = α := by
657+
simp [IsAdjoinRoot.mkOfAdjoinEqTop, IsAdjoinRoot.root]
536658

537-
@[deprecated (since := "2025-08-13")] alias aequiv_self := algEquiv_self
659+
end mkOfAdjoinEqTop
538660

539-
@[simp]
540-
theorem algEquiv_symm (h' : IsAdjoinRoot T f) : (h.algEquiv h').symm = h'.algEquiv h := rfl
661+
section Equiv
541662

542-
@[deprecated (since := "2025-08-13")] alias aequiv_symm := algEquiv_symm
663+
variable {T : Type*} [CommRing T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type*} [CommRing U]
543664

544665
@[simp]
545-
theorem lift_algEquiv {U : Type*} [CommRing U] (h' : IsAdjoinRoot T f) (i : R →+* U) (x hx z) :
546-
h'.lift i x hx (h.algEquiv h' z) = h.lift i x hx z := by
547-
rw [← h.map_repr z, algEquiv_map, lift_map, lift_map]
666+
theorem lift_algEquiv (i : R →+* U) (x hx z) :
667+
h'.lift i x hx (h.algEquiv h' z) = h.lift i x hx z := by rw [← h.map_repr z]; simp [- map_repr]
548668

549669
@[deprecated (since := "2025-08-13")] alias lift_aequiv := lift_algEquiv
550670

551671
@[simp]
552-
theorem liftHom_algEquiv {U : Type*} [CommRing U] [Algebra R U] (h' : IsAdjoinRoot T f)
553-
(x : U) (hx z) : h'.liftHom x hx (h.algEquiv h' z) = h.liftHom x hx z :=
554-
h.lift_algEquiv h' _ _ hx _
672+
theorem liftHom_algEquiv [Algebra R U] (x : U) (hx z) :
673+
h'.liftHom x hx (h.algEquiv h' z) = h.liftHom x hx z := h.lift_algEquiv h' _ _ hx _
555674

556675
@[deprecated (since := "2025-08-13")] alias liftHom_aequiv := liftHom_algEquiv
557676

558-
@[simp]
559-
theorem algEquiv_algEquiv {U : Type*} [CommRing U] [Algebra R U]
560-
(h' : IsAdjoinRoot T f) (h'' : IsAdjoinRoot U f) (x) :
561-
(h'.algEquiv h'') (h.algEquiv h' x) = h.algEquiv h'' x :=
562-
h.liftHom_algEquiv _ _ h''.aeval_root_self _
563-
564-
@[deprecated (since := "2025-08-13")] alias aequiv_aequiv := algEquiv_algEquiv
565-
566-
@[simp]
567-
theorem algEquiv_trans {U : Type*} [CommRing U] [Algebra R U]
568-
(h' : IsAdjoinRoot T f) (h'' : IsAdjoinRoot U f) :
569-
(h.algEquiv h').trans (h'.algEquiv h'') = h.algEquiv h'' := by
570-
ext z
571-
exact h.algEquiv_algEquiv h' h'' z
572-
573-
@[deprecated (since := "2025-08-13")] alias aequiv_trans := algEquiv_trans
574-
575-
/-- Transfer `IsAdjoinRoot` across an algebra isomorphism.
576-
577-
This is the converse of `IsAdjoinRoot.algEquiv`: this turns an `AlgEquiv` into an `IsAdjoinRoot`,
578-
and `IsAdjoinRoot.algEquiv` turns an `IsAdjoinRoot` into an `AlgEquiv`.
579-
-/
580-
@[simps! map_apply]
581-
def ofAlgEquiv (e : S ≃ₐ[R] T) : IsAdjoinRoot T f where
582-
map := (e : S →ₐ[R] T).comp h.map
583-
map_surjective := e.surjective.comp h.map_surjective
584-
ker_map := by ext; simp [Ideal.mem_span_singleton]
585-
586-
@[deprecated (since := "2025-08-13")] alias ofEquiv := ofAlgEquiv
587-
588-
@[simp]
589-
theorem ofAlgEquiv_root (e : S ≃ₐ[R] T) : (h.ofAlgEquiv e).root = e h.root := rfl
590-
591-
@[deprecated (since := "2025-08-13")] alias ofEquiv_root := ofAlgEquiv_root
592-
593-
@[simp]
594-
theorem algEquiv_ofAlgEquiv {U : Type*} [CommRing U] [Algebra R U]
595-
(h' : IsAdjoinRoot T f) (e : T ≃ₐ[R] U) :
596-
h.algEquiv (h'.ofAlgEquiv e) = (h.algEquiv h').trans e := by
597-
ext a; rw [← h.map_repr a, algEquiv_map, AlgEquiv.trans_apply, algEquiv_map, ofAlgEquiv_map_apply]
598-
599-
@[deprecated (since := "2025-08-13")] alias aequiv_ofEquiv := algEquiv_ofAlgEquiv
600-
601-
@[simp]
602-
theorem ofAlgEquiv_algEquiv {U : Type*} [CommRing U] [Algebra R U]
603-
(h' : IsAdjoinRoot U f) (e : S ≃ₐ[R] T) :
604-
(h.ofAlgEquiv e).algEquiv h' = e.symm.trans (h.algEquiv h') := by
605-
ext a
606-
rw [← (h.ofAlgEquiv e).map_repr a, algEquiv_map, AlgEquiv.trans_apply, ofAlgEquiv_map_apply,
607-
e.symm_apply_apply, algEquiv_map]
608-
609-
@[deprecated (since := "2025-08-13")] alias ofEquiv_aequiv := ofAlgEquiv_algEquiv
610-
611677
end Equiv
612678

613679
end IsAdjoinRoot
@@ -648,3 +714,29 @@ theorem Algebra.adjoin.powerBasis'_minpoly_gen [IsDomain R] [IsDomain S] [NoZero
648714
end Algebra
649715

650716
end CommRing
717+
718+
section Field
719+
720+
open scoped IntermediateField
721+
722+
variable {F E : Type*} [Field F] [Field E] [Algebra F E] {f : F[X]}
723+
724+
namespace IsAdjoinRoot
725+
726+
theorem primitive_element_root (h : IsAdjoinRoot E f) : F⟮h.root⟯ = ⊤ :=
727+
IntermediateField.adjoin_eq_top_of_algebra F {h.root} (adjoin_root_eq_top h)
728+
729+
/-- If `α` is primitive in `E/f`, then `E` is given by adjoining a root of `minpoly F α`. -/
730+
abbrev mkOfPrimitiveElement {α : E} (hα : IsIntegral F α) (hα₂ : F⟮α⟯ = ⊤) :
731+
IsAdjoinRoot E (minpoly F α) :=
732+
mkOfAdjoinEqTop hα (Algebra.adjoin_eq_top_of_primitive_element hα hα₂)
733+
734+
/-- If `α` is primitive in `E/f`, then `E` is given by adjoining a root of `minpoly F α`. -/
735+
abbrev _root_.IsAdjoinRootMonic.mkOfPrimitiveElement
736+
{α : E} (hα : IsIntegral F α) (hα₂ : F⟮α⟯ = ⊤) : IsAdjoinRootMonic E (minpoly F α) where
737+
__ := IsAdjoinRoot.mkOfPrimitiveElement hα hα₂
738+
monic := minpoly.monic hα
739+
740+
end IsAdjoinRoot
741+
742+
end Field

0 commit comments

Comments
 (0)