Loogle!

Result

Found 277 declarations mentioning Polynomial.Splits. Of these, only the first 200 are shown.

• Polynomial.Splits 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] (f : Polynomial R) : Prop
• Polynomial.Splits.X 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] : Polynomial.X.Splits
• Polynomial.Splits.one 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] : Polynomial.Splits 1
• Polynomial.Splits.zero 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] : Polynomial.Splits 0
• Polynomial.splits_of_natDegree_eq_zero 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.natDegree = 0) : f.Splits
• Polynomial.Splits.of_natDegree_eq_zero 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.natDegree = 0) : f.Splits
• Polynomial.splits_of_natDegree_le_one_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.natDegree ≤ 1) (h : f.Monic) : f.Splits
• Polynomial.Splits.of_natDegree_le_one_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.natDegree ≤ 1) (h : f.Monic) : f.Splits
• Polynomial.Splits.of_natDegree_eq_one 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [DivisionSemiring R] {f : Polynomial R} (hf : f.natDegree = 1) : f.Splits
• Polynomial.Splits.of_natDegree_le_one 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [DivisionSemiring R] {f : Polynomial R} (hf : f.natDegree ≤ 1) : f.Splits
• Polynomial.Splits.neg 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Ring R] {f : Polynomial R} (hf : f.Splits) : (-f).Splits
• Polynomial.splits_neg_iff 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Ring R] {f : Polynomial R} : (-f).Splits ↔ f.Splits
• Polynomial.Splits.map 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.Splits) {S : Type u_2} [Semiring S] (i : R →+* S) : (Polynomial.map i f).Splits
• Polynomial.Splits.of_degree_eq_one 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [DivisionSemiring R] {f : Polynomial R} (hf : f.degree = 1) : f.Splits
• IsUnit.splits 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] [NoZeroDivisors R] {f : Polynomial R} (hf : IsUnit f) : f.Splits
• Polynomial.splits_of_degree_le_zero 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.degree ≤ 0) : f.Splits
• Polynomial.Splits.of_degree_le_zero 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.degree ≤ 0) : f.Splits
• Polynomial.splits_of_degree_le_one_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.degree ≤ 1) (h : f.Monic) : f.Splits
• Polynomial.Splits.of_degree_le_one_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.degree ≤ 1) (h : f.Monic) : f.Splits
• Polynomial.Splits.X_pow 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] (n : ℕ) : (Polynomial.X ^ n).Splits
• Polynomial.Splits.comp_neg_X 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Ring R] {f : Polynomial R} (hf : f.Splits) : (f.comp (-Polynomial.X)).Splits
• Polynomial.Splits.mul 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.Splits) : (f * g).Splits
• Polynomial.Splits.of_degree_le_one 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [DivisionSemiring R] {f : Polynomial R} (hf : f.degree ≤ 1) : f.Splits
• Polynomial.rootOfSplits 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Splits) (hfd : f.degree ≠ 0) : R
• Polynomial.splits_of_natDegree_le_one_of_invertible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.natDegree ≤ 1) (h : Invertible f.leadingCoeff) : f.Splits
• Polynomial.Splits.listProd 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {l : List (Polynomial R)} (h : ∀ f ∈ l, f.Splits) : l.prod.Splits
• Polynomial.Splits.natDegree_eq_card_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f.natDegree = f.roots.card
• Polynomial.Splits.of_natDegree_le_one_of_invertible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.natDegree ≤ 1) (h : Invertible f.leadingCoeff) : f.Splits
• Polynomial.splits_iff_card_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] : f.Splits ↔ f.roots.card = f.natDegree
• Polynomial.Splits.pow 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.Splits) (n : ℕ) : (f ^ n).Splits
• Polynomial.Splits.natDegree_le_one_of_irreducible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f : Polynomial R} (hf : f.Splits) (h : Irreducible f) : f.natDegree ≤ 1
• Polynomial.Splits.C 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] (a : R) : (Polynomial.C a).Splits
• Polynomial.Splits.comp_of_natDegree_le_one_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.natDegree ≤ 1) (h : g.Monic) : (f.comp g).Splits
• Polynomial.splits_of_degree_le_one_of_invertible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.degree ≤ 1) (h : Invertible f.leadingCoeff) : f.Splits
• Polynomial.Splits.of_degree_le_one_of_invertible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.degree ≤ 1) (h : Invertible f.leadingCoeff) : f.Splits
• Polynomial.Splits.degree_le_one_of_irreducible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f : Polynomial R} (hf : f.Splits) (h : Irreducible f) : f.degree ≤ 1
• Polynomial.Splits.prod 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {ι : Type u_2} {f : ι → Polynomial R} {s : Finset ι} (h : ∀ i ∈ s, (f i).Splits) : (∏ i ∈ s, f i).Splits
• Polynomial.Splits.roots_ne_zero 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hf0 : f.natDegree ≠ 0) : f.roots ≠ 0
• Polynomial.Splits.multisetProd 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {m : Multiset (Polynomial R)} (hm : ∀ f ∈ m, f.Splits) : m.prod.Splits
• Polynomial.Splits.comp_of_degree_le_one_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.degree ≤ 1) (h : g.Monic) : (f.comp g).Splits
• Polynomial.Splits.X_add_C 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] (a : R) : (Polynomial.X + Polynomial.C a).Splits
• Polynomial.Splits.of_algHom 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (hf : (Polynomial.map (algebraMap R A) f).Splits) (e : A →ₐ[R] B) : (Polynomial.map (algebraMap R B) f).Splits
• Polynomial.splits_iff_comp_splits_of_natDegree_eq_one 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f g : Polynomial R} (hg : g.natDegree = 1) : f.Splits ↔ (f.comp g).Splits
• Polynomial.Splits.comp_of_natDegree_le_one 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f g : Polynomial R} (hf : f.Splits) (hg : g.natDegree ≤ 1) : (f.comp g).Splits
• Polynomial.Splits.exists_eval_eq_zero 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Splits) (hf0 : f.degree ≠ 0) : ∃ a, Polynomial.eval a f = 0
• Polynomial.Splits.natDegree_eq_one_of_irreducible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f : Polynomial R} (hf : f.Splits) (h : Irreducible f) : f.natDegree = 1
• Polynomial.Splits.of_natDegree_eq_two 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f : Polynomial R} {x : R} (h₁ : f.natDegree = 2) (h₂ : Polynomial.eval x f = 0) : f.Splits
• Polynomial.eval_rootOfSplits 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Splits) (hfd : f.degree ≠ 0) : Polynomial.eval (Polynomial.rootOfSplits hf hfd) f = 0
• Polynomial.Splits.comp_of_natDegree_le_one_of_invertible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.natDegree ≤ 1) (h : Invertible g.leadingCoeff) : (f.comp g).Splits
• Polynomial.Splits.C_mul 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.Splits) (a : R) : (Polynomial.C a * f).Splits
• Polynomial.Splits.nextCoeff_eq_neg_sum_roots_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) : f.nextCoeff = -f.roots.sum
• Polynomial.splits_iff_comp_splits_of_degree_eq_one 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f g : Polynomial R} (hg : g.degree = 1) : f.Splits ↔ (f.comp g).Splits
• Polynomial.Splits.degree_eq_one_of_irreducible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f : Polynomial R} (hf : f.Splits) (h : Irreducible f) : f.degree = 1
• Polynomial.Splits.of_X_mul 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] : (Polynomial.X * f).Splits → f.Splits
• Polynomial.Splits.of_mul_X 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] : (f * Polynomial.X).Splits → f.Splits
• Polynomial.splits_X_mul 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] : (Polynomial.X * f).Splits ↔ f.Splits
• Polynomial.splits_mul_X 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] : (f * Polynomial.X).Splits ↔ f.Splits
• Polynomial.Splits.eval_eq_prod_roots_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) (x : R) : Polynomial.eval x f = (Multiset.map (fun x_1 => x - x_1) f.roots).prod
• Polynomial.Splits.comp_of_degree_le_one 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f g : Polynomial R} (hf : f.Splits) (hg : g.degree ≤ 1) : (f.comp g).Splits
• Polynomial.Splits.comp_of_degree_le_one_of_invertible 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.degree ≤ 1) (h : Invertible g.leadingCoeff) : (f.comp g).Splits
• Polynomial.Splits.degree_eq_card_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hf0 : f ≠ 0) : f.degree = ↑f.roots.card
• Polynomial.Splits.of_degree_eq_two 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f : Polynomial R} {x : R} (h₁ : f.degree = 2) (h₂ : Polynomial.eval x f = 0) : f.Splits
• Polynomial.Splits.monomial 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] (n : ℕ) (a : R) : ((Polynomial.monomial n) a).Splits
• Polynomial.Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f.nextCoeff = -f.leadingCoeff * f.roots.sum
• Polynomial.Splits.eval_eq_prod_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (x : R) : Polynomial.eval x f = f.leadingCoeff * (Multiset.map (fun x_1 => x - x_1) f.roots).prod
• Polynomial.Splits.of_isScalarTower 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f : Polynomial R} {A : Type u_2} (B : Type u_3) [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (hf : (Polynomial.map (algebraMap R A) f).Splits) : (Polynomial.map (algebraMap R B) f).Splits
• Polynomial.Splits.C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Semiring R] (a : R) (n : ℕ) : (Polynomial.C a * Polynomial.X ^ n).Splits
• Polynomial.Splits.X_sub_C 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Ring R] (a : R) : (Polynomial.X - Polynomial.C a).Splits
• Polynomial.map_sub_sprod_roots_eq_prod_map_eval 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] [IsDomain R] (s : Multiset R) (g : Polynomial R) (hg : g.Monic) (hg' : g.Splits) : (Multiset.map (fun ij => ij.1 - ij.2) (s ×ˢ g.roots)).prod = (Multiset.map (fun x => Polynomial.eval x g) s).prod
• Polynomial.Splits.comp_X_add_C 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f : Polynomial R} (hf : f.Splits) (a : R) : (f.comp (Polynomial.X + Polynomial.C a)).Splits
• Polynomial.splits_mul_iff_left 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f g : Polynomial R} [IsDomain R] (hg₀ : g ≠ 0) (hg : g.Splits) : (f * g).Splits ↔ f.Splits
• Polynomial.splits_mul_iff_right 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f g : Polynomial R} [IsDomain R] (hf₀ : f ≠ 0) (hg : f.Splits) : (f * g).Splits ↔ g.Splits
• Polynomial.splits_prod_iff 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] [IsDomain R] {ι : Type u_4} {f : ι → Polynomial R} {s : Finset ι} (hf : ∀ i ∈ s, f i ≠ 0) : (∏ x ∈ s, f x).Splits ↔ ∀ x ∈ s, (f x).Splits
• Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) : f.coeff 0 = (-1) ^ f.natDegree * f.roots.prod
• Polynomial.Splits.roots_map 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} {S : Type u_2} [Field R] [CommRing S] [IsDomain S] {f : Polynomial R} (hf : f.Splits) (i : R →+* S) : (Polynomial.map i f).roots = Multiset.map (⇑i) f.roots
• Polynomial.Splits.of_dvd 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f g : Polynomial R} [IsDomain R] (hg : g.Splits) (hg₀ : g ≠ 0) (hfg : f ∣ g) : f.Splits
• Polynomial.Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f.coeff 0 = (-1) ^ f.natDegree * f.leadingCoeff * f.roots.prod
• Polynomial.Splits.of_splits_map 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} {S : Type u_2} [Field R] [CommRing S] [IsDomain S] {f : Polynomial R} (i : R →+* S) (hf : (Polynomial.map i f).Splits) (hi : ∀ a ∈ (Polynomial.map i f).roots, a ∈ i.range) : f.Splits
• Polynomial.splits_mul 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f g : Polynomial R} [IsDomain R] (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) : (f * g).Splits ↔ f.Splits ∧ g.Splits
• Polynomial.splits_mul_iff 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f g : Polynomial R} [IsDomain R] (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) : (f * g).Splits ↔ f.Splits ∧ g.Splits
• Polynomial.splits_mul' 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f g : Polynomial R} [IsDomain R] : (f * g).Splits ↔ (f.Splits ∨ g = 0) ∧ (g.Splits ∨ f = 0)
• Polynomial.Splits.comp_X_sub_C 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Splits) (a : R) : (f.comp (Polynomial.X - Polynomial.C a)).Splits
• Polynomial.Splits.mem_range_of_isRoot 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} {S : Type u_2} [Field R] [CommRing S] [IsDomain S] {f : Polynomial R} (hf : f.Splits) (hf0 : f ≠ 0) {i : R →+* S} {x : S} (hx : (Polynomial.map i f).IsRoot x) : x ∈ i.range
• Polynomial.Splits.roots_map_of_injective 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] {S : Type u_4} [CommRing S] [IsDomain S] (hf : f.Splits) {i : R →+* S} (hi : Function.Injective ⇑i) : (Polynomial.map i f).roots = Multiset.map (⇑i) f.roots
• Polynomial.Splits.roots_map_of_ne_zero 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] [IsDomain R] {S : Type u_4} [CommRing S] [IsDomain S] {f : Polynomial R} (hf : f.Splits) {φ : R →+* S} (hφ : Polynomial.map φ f ≠ 0) : (Polynomial.map φ f).roots = Multiset.map (⇑φ) f.roots
• Polynomial.Splits.of_splits_map_of_injective 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} {S : Type u_4} [CommRing S] [IsDomain S] {i : R →+* S} (hi : Function.Injective ⇑i) (hf : (Polynomial.map i f).Splits) : (∀ a ∈ (Polynomial.map i f).roots, a ∈ i.range) → f.Splits
• Polynomial.Splits.dvd_of_roots_le_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f g : Polynomial R} (hp : f.Splits) (hp0 : f ≠ 0) (hq : f.roots ≤ g.roots) : f ∣ g
• Polynomial.Splits.image_rootSet 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [Field A] [Algebra R A] [CommRing B] [IsDomain B] [Algebra R B] {f : Polynomial R} (hf : (Polynomial.map (algebraMap R A) f).Splits) (g : A →ₐ[R] B) : ⇑g '' f.rootSet A = f.rootSet B
• Polynomial.map_sub_roots_sprod_eq_prod_map_eval 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] [IsDomain R] (s : Multiset R) (g : Polynomial R) (hg : g.Monic) (hg' : g.Splits) : (Multiset.map (fun ij => ij.1 - ij.2) (g.roots ×ˢ s)).prod = (-1) ^ (s.card * g.roots.card) * (Multiset.map (fun x => Polynomial.eval x g) s).prod
• Polynomial.splits_X_sub_C_mul_iff 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] {a : R} : ((Polynomial.X - Polynomial.C a) * f).Splits ↔ f.Splits
• Polynomial.Splits.taylor 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {p : Polynomial R} (hp : p.Splits) (r : R) : ((Polynomial.taylor r) p).Splits
• Polynomial.Splits.eq_prod_roots_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) : f = (Multiset.map (fun x => Polynomial.X - Polynomial.C x) f.roots).prod
• Polynomial.Splits.mem_lift_of_roots_mem_range 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) {S : Type u_4} [Ring S] (i : S →+* R) (hr : ∀ a ∈ f.roots, a ∈ i.range) : f ∈ Polynomial.lifts i
• Polynomial.Splits.image_rootSet_algebraMap 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [CommRing B] [IsDomain B] [Algebra R B] [Algebra A B] [FaithfulSMul A B] [IsScalarTower R A B] {f : Polynomial R} (hf : (Polynomial.map (algebraMap R A) f).Splits) : ⇑(algebraMap A B) '' f.rootSet A = f.rootSet B
• Polynomial.Splits.map_aroots_algebraMap 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [CommRing B] [IsDomain B] [Algebra R B] [Algebra A B] [FaithfulSMul A B] [IsScalarTower R A B] {f : Polynomial R} (hf : (Polynomial.map (algebraMap R A) f).Splits) : Multiset.map (⇑(algebraMap A B)) (f.aroots A) = f.aroots B
• Polynomial.Splits.dvd_iff_roots_le_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f g : Polynomial R} (hf : f.Splits) (hf0 : f ≠ 0) (hg0 : g ≠ 0) : f ∣ g ↔ f.roots ≤ g.roots
• Polynomial.Splits.aeval_eq_prod_aroots_of_monic 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} [CommRing A] [IsDomain A] [Algebra R A] (hf : (Polynomial.map (algebraMap R A) f).Splits) (hm : f.Monic) (x : A) : (Polynomial.aeval x) f = (Multiset.map (fun x_1 => x - x_1) (f.aroots A)).prod
• Polynomial.Splits.image_rootSet_of_map_ne_zero 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] [Algebra R A] [Algebra R B] (hf : (Polynomial.map (algebraMap R A) f).Splits) (φ : A →ₐ[R] B) (hφ : Polynomial.map (algebraMap R B) f ≠ 0) : ⇑φ '' f.rootSet A = f.rootSet B
• Polynomial.splits_iff_exists_multiset' 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommSemiring R] {f : Polynomial R} : f.Splits ↔ ∃ m, f = Polynomial.C f.leadingCoeff * (Multiset.map (fun x => Polynomial.X + Polynomial.C x) m).prod
• Polynomial.Splits.eq_X_sub_C_of_single_root 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) {x : R} (hr : f.roots = {x}) : f = Polynomial.C f.leadingCoeff * (Polynomial.X - Polynomial.C x)
• Polynomial.splits_iff_exists_multiset 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} : f.Splits ↔ ∃ m, f = Polynomial.C f.leadingCoeff * (Multiset.map (fun x => Polynomial.X - Polynomial.C x) m).prod
• Polynomial.Splits.eq_prod_roots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f = Polynomial.C f.leadingCoeff * (Multiset.map (fun x => Polynomial.X - Polynomial.C x) f.roots).prod
• Polynomial.Splits.eval_root_derivative 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] [DecidableEq R] (hf : f.Splits) (hm : f.Monic) {x : R} (hx : x ∈ f.roots) : Polynomial.eval x (Polynomial.derivative f) = (Multiset.map (fun x_1 => x - x_1) (f.roots.erase x)).prod
• Polynomial.Splits.aeval_eq_prod_aroots 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} {S : Type u_2} [Field R] [CommRing S] [IsDomain S] [Algebra R S] {f : Polynomial R} (hf : (Polynomial.map (algebraMap R S) f).Splits) (x : S) : (Polynomial.aeval x) f = (algebraMap R S) f.leadingCoeff * (Multiset.map (fun x_1 => x - x_1) (f.aroots S)).prod
• Polynomial.Splits.eval_derivative 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] [DecidableEq R] (hf : f.Splits) (x : R) : Polynomial.eval x (Polynomial.derivative f) = f.leadingCoeff * (Multiset.map (fun a => (Multiset.map (fun x_1 => x - x_1) (f.roots.erase a)).prod) f.roots).sum
• Polynomial.Splits.adjoin_rootSet_eq_range 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [Field A] [Algebra R A] [CommRing B] [IsDomain B] [Algebra R B] {f : Polynomial R} (hf : (Polynomial.map (algebraMap R A) f).Splits) (g : A →ₐ[R] B) : Algebra.adjoin R (f.rootSet B) = g.range ↔ Algebra.adjoin R (f.rootSet A) = ⊤
• Polynomial.Splits.eval_derivative_div_eval_of_ne_zero 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f : Polynomial R} (hf : f.Splits) {x : R} (hx : Polynomial.eval x f ≠ 0) : Polynomial.eval x (Polynomial.derivative f) / Polynomial.eval x f = (Multiset.map (fun z => 1 / (x - z)) f.roots).sum
• Polynomial.Splits.eval_derivative_eq_eval_mul_sum 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f : Polynomial R} (hf : f.Splits) {x : R} (hx : Polynomial.eval x f ≠ 0) : Polynomial.eval x (Polynomial.derivative f) = Polynomial.eval x f * (Multiset.map (fun z => 1 / (x - z)) f.roots).sum
• Polynomial.Splits.mem_subfield_of_isRoot 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] (F : Subfield R) {f : Polynomial ↥F} (hf : f.Splits) (hf0 : f ≠ 0) {x : R} (hx : (Polynomial.map F.subtype f).IsRoot x) : x ∈ F
• Polynomial.Splits.scaleRoots 📋 Mathlib.RingTheory.Polynomial.ScaleRoots
  {R : Type u_1} [CommSemiring R] {p : Polynomial R} (hp : p.Splits) (r : R) : (p.scaleRoots r).Splits
• Cubic.splits_iff_card_roots 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} (ha : P.a ≠ 0) : (Polynomial.map φ P.toPoly).Splits ↔ (Cubic.map φ P).roots.card = 3
• Cubic.discr_ne_zero_iff_roots_nodup 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} (ha : P.a ≠ 0) (hP : (Polynomial.map φ P.toPoly).Splits) : P.discr ≠ 0 ↔ (Cubic.map φ P).roots.Nodup
• Cubic.splits_iff_roots_eq_three 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} (ha : P.a ≠ 0) : (Polynomial.map φ P.toPoly).Splits ↔ ∃ x y z, (Cubic.map φ P).roots = {x, y, z}
• Cubic.card_roots_of_discr_ne_zero 📋 Mathlib.Algebra.CubicDiscriminant
  {F : Type u_3} {K : Type u_4} {P : Cubic F} [Field F] [Field K] {φ : F →+* K} [DecidableEq K] (ha : P.a ≠ 0) (h3 : (Polynomial.map φ P.toPoly).Splits) (hd : P.discr ≠ 0) : (Cubic.map φ P).roots.toFinset.card = 3
• Polynomial.Monic.exists_splits_map 📋 Mathlib.RingTheory.AdjoinRoot
  {R : Type u} [CommRing R] [Nontrivial R] {p : Polynomial R} (hp : p.Monic) : ∃ S x x_1, ∃ (_ : Module.Finite R S) (_ : Module.Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits
• Polynomial.nodup_roots_iff_of_splits 📋 Mathlib.FieldTheory.Separable
  {F : Type u} [Field F] {f : Polynomial F} (hf : f ≠ 0) (h : f.Splits) : f.roots.Nodup ↔ f.Separable
• Polynomial.card_rootSet_eq_natDegree 📋 Mathlib.FieldTheory.Separable
  {F : Type u} [Field F] {K : Type v} [Field K] [Algebra F K] {p : Polynomial F} (hsep : p.Separable) (hsplit : (Polynomial.map (algebraMap F K) p).Splits) : Fintype.card ↑(p.rootSet K) = p.natDegree
• Polynomial.nodup_aroots_iff_of_splits 📋 Mathlib.FieldTheory.Separable
  {F : Type u} [Field F] {K : Type v} [Field K] [Algebra F K] {f : Polynomial F} (hf : f ≠ 0) (h : (Polynomial.map (algebraMap F K) f).Splits) : (f.aroots K).Nodup ↔ f.Separable
• AlgHom.natCard_of_powerBasis 📋 Mathlib.FieldTheory.Separable
  {S : Type u_1} [CommRing S] {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K S] [Algebra K L] (pb : PowerBasis K S) (h_sep : IsSeparable K pb.gen) (h_splits : (Polynomial.map (algebraMap K L) (minpoly K pb.gen)).Splits) : Nat.card (S →ₐ[K] L) = pb.dim
• Polynomial.card_rootSet_eq_natDegree_iff_of_splits 📋 Mathlib.FieldTheory.Separable
  {F : Type u} [Field F] {K : Type v} [Field K] [Algebra F K] {f : Polynomial F} (hf : f ≠ 0) (h : (Polynomial.map (algebraMap F K) f).Splits) : Fintype.card ↑(f.rootSet K) = f.natDegree ↔ f.Separable
• AlgHom.card_of_powerBasis 📋 Mathlib.FieldTheory.Separable
  {S : Type u_1} [CommRing S] {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K S] [Algebra K L] (pb : PowerBasis K S) (h_sep : IsSeparable K pb.gen) (h_splits : (Polynomial.map (algebraMap K L) (minpoly K pb.gen)).Splits) : Fintype.card (S →ₐ[K] L) = pb.dim
• Polynomial.exists_finset_of_splits 📋 Mathlib.FieldTheory.Separable
  {F : Type u} [Field F] {K : Type v} [Field K] (i : F →+* K) {f : Polynomial F} (sep : f.Separable) (sp : (Polynomial.map i f).Splits) : ∃ s, Polynomial.map i f = Polynomial.C (i f.leadingCoeff) * ∏ a ∈ s, (Polynomial.X - Polynomial.C a)
• Polynomial.eq_X_sub_C_of_separable_of_root_eq 📋 Mathlib.FieldTheory.Separable
  {F : Type u} [Field F] {K : Type v} [Field K] {i : F →+* K} {x : F} {h : Polynomial F} (h_sep : h.Separable) (h_root : Polynomial.eval x h = 0) (h_splits : (Polynomial.map i h).Splits) (h_roots : ∀ y ∈ (Polynomial.map i h).roots, y = i x) : h = Polynomial.C h.leadingCoeff * (Polynomial.X - Polynomial.C x)
• Normal.splits 📋 Mathlib.FieldTheory.Normal.Defs
  {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] : Normal F K → ∀ (x : K), (Polynomial.map (algebraMap F K) (minpoly F x)).Splits
• Normal.splits' 📋 Mathlib.FieldTheory.Normal.Defs
  {F : Type u_1} {K : Type u_2} {inst✝ : Field F} {inst✝¹ : Field K} {inst✝² : Algebra F K} [self : Normal F K] (x : K) : (Polynomial.map (algebraMap F K) (minpoly F x)).Splits
• Normal.mk 📋 Mathlib.FieldTheory.Normal.Defs
  {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [toIsAlgebraic : Algebra.IsAlgebraic F K] (splits' : ∀ (x : K), (Polynomial.map (algebraMap F K) (minpoly F x)).Splits) : Normal F K
• Normal.out 📋 Mathlib.FieldTheory.Normal.Defs
  {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] : Normal F K → ∀ (x : K), IsIntegral F x ∧ (Polynomial.map (algebraMap F K) (minpoly F x)).Splits
• normal_iff 📋 Mathlib.FieldTheory.Normal.Defs
  {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] : Normal F K ↔ ∀ (x : K), IsIntegral F x ∧ (Polynomial.map (algebraMap F K) (minpoly F x)).Splits
• minpoly_neg_splits 📋 Mathlib.RingTheory.Adjoin.Field
  {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] {x : L} (g : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits) : (Polynomial.map (algebraMap K L) (minpoly K (-x))).Splits
• IsIntegral.mem_range_algHom_of_minpoly_splits 📋 Mathlib.RingTheory.Adjoin.Field
  {R : Type u_1} {K : Type u_2} {L : Type u_3} [CommRing R] [Field K] [Field L] [Algebra R K] {x : L} [Algebra R L] (int : IsIntegral R x) (h : (Polynomial.map (algebraMap R K) (minpoly R x)).Splits) (f : K →ₐ[R] L) : x ∈ f.range
• minpoly_add_algebraMap_splits 📋 Mathlib.RingTheory.Adjoin.Field
  {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] {x : L} (r : K) (g : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits) : (Polynomial.map (algebraMap K L) (minpoly K (x + (algebraMap K L) r))).Splits
• minpoly_algebraMap_add_splits 📋 Mathlib.RingTheory.Adjoin.Field
  {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] {x : L} (r : K) (g : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits) : (Polynomial.map (algebraMap K L) (minpoly K ((algebraMap K L) r + x))).Splits
• minpoly_algebraMap_sub_splits 📋 Mathlib.RingTheory.Adjoin.Field
  {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] {x : L} (r : K) (g : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits) : (Polynomial.map (algebraMap K L) (minpoly K ((algebraMap K L) r - x))).Splits
• minpoly_sub_algebraMap_splits 📋 Mathlib.RingTheory.Adjoin.Field
  {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] {x : L} (r : K) (g : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits) : (Polynomial.map (algebraMap K L) (minpoly K (x - (algebraMap K L) r))).Splits
• IsIntegral.mem_range_algebraMap_of_minpoly_splits 📋 Mathlib.RingTheory.Adjoin.Field
  {R : Type u_1} {K : Type u_2} {L : Type u_3} [CommRing R] [Field K] [Field L] [Algebra R K] {x : L} [Algebra R L] [Algebra K L] [IsScalarTower R K L] (int : IsIntegral R x) (h : (Polynomial.map (algebraMap R K) (minpoly R x)).Splits) : x ∈ (algebraMap K L).range
• IsIntegral.minpoly_splits_tower_top' 📋 Mathlib.RingTheory.Adjoin.Field
  {R : Type u_1} {K : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [Field K] [Field L] [CommRing M] [Algebra R K] [Algebra R M] [Algebra K M] [IsScalarTower R K M] {x : M} (int : IsIntegral R x) {f : K →+* L} (h : (Polynomial.map (f.comp (algebraMap R K)) (minpoly R x)).Splits) : (Polynomial.map f (minpoly K x)).Splits
• IsIntegral.minpoly_splits_tower_top 📋 Mathlib.RingTheory.Adjoin.Field
  {R : Type u_1} {K : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [Field K] [Field L] [CommRing M] [Algebra R K] [Algebra R M] [Algebra K M] [IsScalarTower R K M] {x : M} [Algebra K L] [Algebra R L] [IsScalarTower R K L] (int : IsIntegral R x) (h : (Polynomial.map (algebraMap R L) (minpoly R x)).Splits) : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
• Polynomial.lift_of_splits 📋 Mathlib.RingTheory.Adjoin.Field
  {F : Type u_2} {K : Type u_3} {L : Type u_4} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] (s : Finset K) : (∀ x ∈ s, IsIntegral F x ∧ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
• Polynomial.IsSplittingField.splits 📋 Mathlib.FieldTheory.SplittingField.IsSplittingField
  {K : Type v} (L : Type w) [Field K] [Field L] [Algebra K L] (f : Polynomial K) [Polynomial.IsSplittingField K L f] : (Polynomial.map (algebraMap K L) f).Splits
• Polynomial.IsSplittingField.splits' 📋 Mathlib.FieldTheory.SplittingField.IsSplittingField
  {K : Type v} {L : Type w} {inst✝ : Field K} {inst✝¹ : Field L} {inst✝² : Algebra K L} {f : Polynomial K} [self : Polynomial.IsSplittingField K L f] : (Polynomial.map (algebraMap K L) f).Splits
• Polynomial.IsSplittingField.lift 📋 Mathlib.FieldTheory.SplittingField.IsSplittingField
  {F : Type u} {K : Type v} (L : Type w) [Field K] [Field L] [Field F] [Algebra K L] [Algebra K F] (f : Polynomial K) [Polynomial.IsSplittingField K L f] (hf : (Polynomial.map (algebraMap K F) f).Splits) : L →ₐ[K] F
• isSplittingField_iff_intermediateField 📋 Mathlib.FieldTheory.SplittingField.IsSplittingField
  {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {p : Polynomial K} : Polynomial.IsSplittingField K L p ↔ (Polynomial.map (algebraMap K L) p).Splits ∧ IntermediateField.adjoin K (p.rootSet L) = ⊤
• IntermediateField.adjoin_rootSet_isSplittingField 📋 Mathlib.FieldTheory.SplittingField.IsSplittingField
  {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {p : Polynomial K} (hp : (Polynomial.map (algebraMap K L) p).Splits) : Polynomial.IsSplittingField K (↥(IntermediateField.adjoin K (p.rootSet L))) p
• Polynomial.IsSplittingField.mk 📋 Mathlib.FieldTheory.SplittingField.IsSplittingField
  {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {f : Polynomial K} (splits' : (Polynomial.map (algebraMap K L) f).Splits) (adjoin_rootSet' : Algebra.adjoin K (f.rootSet L) = ⊤) : Polynomial.IsSplittingField K L f
• Polynomial.IsSplittingField.IsScalarTower.splits 📋 Mathlib.FieldTheory.SplittingField.IsSplittingField
  {F : Type u} {K : Type v} (L : Type w) [Field K] [Field L] [Field F] [Algebra K L] [Algebra F K] [Algebra F L] [IsScalarTower F K L] (f : Polynomial F) [Polynomial.IsSplittingField K L ((Polynomial.mapAlg F K) f)] : ((Polynomial.mapAlg F L) f).Splits
• IsIntegral.mem_intermediateField_of_minpoly_splits 📋 Mathlib.FieldTheory.SplittingField.IsSplittingField
  {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {x : L} (int : IsIntegral K x) {F : IntermediateField K L} (h : (Polynomial.map (algebraMap K ↥F) (minpoly K x)).Splits) : x ∈ F
• IntermediateField.splits_of_splits 📋 Mathlib.FieldTheory.SplittingField.IsSplittingField
  {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {p : Polynomial K} {F : IntermediateField K L} (h : (Polynomial.map (algebraMap K L) p).Splits) (hF : ∀ x ∈ p.rootSet L, x ∈ F) : (Polynomial.map (algebraMap K ↥F) p).Splits
• IntermediateField.splits_iff_mem 📋 Mathlib.FieldTheory.SplittingField.IsSplittingField
  {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {p : Polynomial K} {F : IntermediateField K L} (h : (Polynomial.map (algebraMap K L) p).Splits) : (Polynomial.map (algebraMap K ↥F) p).Splits ↔ ∀ x ∈ p.rootSet L, x ∈ F
• Polynomial.IsSplittingField.splits_iff 📋 Mathlib.FieldTheory.SplittingField.IsSplittingField
  {K : Type v} (L : Type w) [Field K] [Field L] [Algebra K L] (f : Polynomial K) [Polynomial.IsSplittingField K L f] : f.Splits ↔ ⊤ = ⊥
• IntermediateField.isSplittingField_iff 📋 Mathlib.FieldTheory.SplittingField.IsSplittingField
  {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {p : Polynomial K} {F : IntermediateField K L} : Polynomial.IsSplittingField K (↥F) p ↔ (Polynomial.map (algebraMap K ↥F) p).Splits ∧ F = IntermediateField.adjoin K (p.rootSet L)
• Polynomial.Irreducible.natDegree_dvd_finrank 📋 Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
  {K : Type u} [Field K] {L : Type u_3} [Field L] [Algebra K L] {f : Polynomial K} (hi : Irreducible f) (hs : (Polynomial.map (algebraMap K L) f).Splits) : f.natDegree ∣ Module.finrank K L
• IntermediateField.card_algHom_adjoin_integral 📋 Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
  (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : Type u} [Field K] [Algebra F K] (h : IsIntegral F α) (h_sep : IsSeparable F α) (h_splits : (Polynomial.map (algebraMap F K) (minpoly F α)).Splits) : Nat.card (↥F⟮α⟯ →ₐ[F] K) = (minpoly F α).natDegree
• IntermediateField.nonempty_algHom_of_splits 📋 Mathlib.FieldTheory.Extension
  {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] (hK' : ∀ (s : E), IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) : Nonempty (E →ₐ[F] K)
• IntermediateField.Lifts.exists_lift_of_splits 📋 Mathlib.FieldTheory.Extension
  {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] (x : IntermediateField.Lifts F E K) {s : E} (h1 : IsIntegral F s) (h2 : (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) : ∃ y, x ≤ y ∧ s ∈ y.carrier
• Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits 📋 Mathlib.FieldTheory.Extension
  {F : Type u_1} {K : Type u_2} (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F L] [Algebra F K] (hA : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) [Algebra.IsAlgebraic F K] (x : K) : (Set.range fun ψ => ψ x) = (minpoly F x).rootSet L
• IntermediateField.nonempty_algHom_of_adjoin_splits 📋 Mathlib.FieldTheory.Extension
  {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} (hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) (hS : IntermediateField.adjoin F S = ⊤) : Nonempty (E →ₐ[F] K)
• IntermediateField.exists_algHom_of_splits' 📋 Mathlib.FieldTheory.Extension
  {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {L : Type u_4} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] (f : L →ₐ[F] K) (hK : ∀ (s : E), IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits) : ∃ φ, AlgHom.domRestrict L φ = f
• IntermediateField.nonempty_algHom_adjoin_of_splits 📋 Mathlib.FieldTheory.Extension
  {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} (hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) : Nonempty (↥(IntermediateField.adjoin F S) →ₐ[F] K)
• IntermediateField.exists_algHom_of_splits_of_aeval 📋 Mathlib.FieldTheory.Extension
  {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] (hK' : ∀ (s : E), IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) {x : E} {y : K} (hy : (Polynomial.aeval y) (minpoly F x) = 0) : ∃ φ, φ x = y
• IntermediateField.exists_algHom_of_adjoin_splits' 📋 Mathlib.FieldTheory.Extension
  {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} {L : Type u_4} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] (f : L →ₐ[F] K) (hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits) (hS : IntermediateField.adjoin L S = ⊤) : ∃ φ, AlgHom.domRestrict L φ = f
• IntermediateField.exists_algHom_of_adjoin_splits_of_aeval 📋 Mathlib.FieldTheory.Extension
  {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} (hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) {x : E} {y : K} (hS : IntermediateField.adjoin F S = ⊤) (hy : (Polynomial.aeval y) (minpoly F x) = 0) : ∃ φ, φ x = y
• IntermediateField.Lifts.exists_lift_of_splits' 📋 Mathlib.FieldTheory.Extension
  {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] (x : IntermediateField.Lifts F E K) {s : E} (h1 : IsIntegral (↥x.carrier) s) (h2 : (Polynomial.map x.emb.toRingHom (minpoly (↥x.carrier) s)).Splits) : ∃ y, x ≤ y ∧ s ∈ y.carrier
• IntermediateField.exists_algHom_of_splits 📋 Mathlib.FieldTheory.Extension
  {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] (hK' : ∀ (s : E), IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) {L : IntermediateField F E} (f : ↥L →ₐ[F] K) : ∃ φ, φ.comp L.val = f
• IntermediateField.exists_algHom_adjoin_of_splits' 📋 Mathlib.FieldTheory.Extension
  {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} {L : Type u_4} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] (f : L →ₐ[F] K) (hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits) : ∃ φ, AlgHom.domRestrict L φ = f
• IntermediateField.exists_algHom_of_adjoin_splits 📋 Mathlib.FieldTheory.Extension
  {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} (hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) {L : IntermediateField F E} (f : ↥L →ₐ[F] K) (hS : IntermediateField.adjoin F S = ⊤) : ∃ φ, φ.comp L.val = f
• IntermediateField.exists_algHom_adjoin_of_splits_of_aeval 📋 Mathlib.FieldTheory.Extension
  {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} (hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) {x : E} {y : K} (hx : x ∈ IntermediateField.adjoin F S) (hy : (Polynomial.aeval y) (minpoly F x) = 0) : ∃ φ, φ ⟨x, hx⟩ = y
• IntermediateField.exists_algHom_adjoin_of_splits 📋 Mathlib.FieldTheory.Extension
  {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} (hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) {L : IntermediateField F E} (f : ↥L →ₐ[F] K) (hL : L ≤ IntermediateField.adjoin F S) : ∃ φ, φ.comp (IntermediateField.inclusion hL) = f
• IsAlgClosed.mk 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] (splits : ∀ (p : Polynomial k), p.Splits) : IsAlgClosed k
• IsAlgClosed.splits 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} {inst✝ : Field k} [self : IsAlgClosed k] (p : Polynomial k) : p.Splits
• IsAlgClosed.splits_domain 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u_1} {K : Type u_2} [Field k] [IsAlgClosed k] [Field K] {f : k →+* K} (p : Polynomial k) : (Polynomial.map f p).Splits
• IsAlgClosure.of_splits 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [Algebra.IsIntegral R K] [Module.IsTorsionFree R K] (h : ∀ (p : Polynomial R), p.Monic → Irreducible p → (Polynomial.map (algebraMap R K) p).Splits) : IsAlgClosure R K
• Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] [Algebra.IsAlgebraic F K] (L : Type u_4) [Field L] [Algebra F L] [Algebra L A] [IsScalarTower F L A] (hL : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) : (K →ₐ[F] L) ≃ (K →ₐ[F] A)
• Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits_apply_apply 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] [Algebra.IsAlgebraic F K] (L : Type u_4) [Field L] [Algebra F L] [Algebra L A] [IsScalarTower F L A] (hL : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) (f : K →ₐ[F] L) (x : K) : ((Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits A L hL) f) x = (algebraMap L A) (f x)
• IntermediateField.algHomEquivAlgHomOfSplits 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] [Algebra.IsAlgebraic F K] (L : IntermediateField F A) (hL : ∀ (x : K), (Polynomial.map (algebraMap F ↥L) (minpoly F x)).Splits) : (K →ₐ[F] ↥L) ≃ (K →ₐ[F] A)
• IntermediateField.algHomEquivAlgHomOfSplits_symm_apply 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] [Algebra.IsAlgebraic F K] (L : IntermediateField F A) (hL : ∀ (x : K), (Polynomial.map (algebraMap F ↥L) (minpoly F x)).Splits) (f : K →ₐ[F] A) : (IntermediateField.algHomEquivAlgHomOfSplits A L hL).symm f = f.codRestrict L.toSubalgebra ⋯
• IntermediateField.algHomEquivAlgHomOfSplits_apply 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] [Algebra.IsAlgebraic F K] (L : IntermediateField F A) (hL : ∀ (x : K), (Polynomial.map (algebraMap F ↥L) (minpoly F x)).Splits) (φ₂ : K →ₐ[F] ↥L) : (IntermediateField.algHomEquivAlgHomOfSplits A L hL) φ₂ = L.val.comp φ₂
• IntermediateField.algHomEquivAlgHomOfSplits_apply_apply 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] [Algebra.IsAlgebraic F K] (L : IntermediateField F A) (hL : ∀ (x : K), (Polynomial.map (algebraMap F ↥L) (minpoly F x)).Splits) (f : K →ₐ[F] ↥L) (x : K) : ((IntermediateField.algHomEquivAlgHomOfSplits A L hL) f) x = (algebraMap (↥L) A) (f x)
• Polynomial.SplittingField.splits 📋 Mathlib.FieldTheory.SplittingField.Construction
  {K : Type v} [Field K] (f : Polynomial K) : (Polynomial.map (algebraMap K f.SplittingField) f).Splits
• Polynomial.SplittingField.lift 📋 Mathlib.FieldTheory.SplittingField.Construction
  {K : Type v} {L : Type w} [Field K] [Field L] (f : Polynomial K) [Algebra K L] (hb : (Polynomial.map (algebraMap K L) f).Splits) : f.SplittingField →ₐ[K] L
• Polynomial.SplittingFieldAux.splits 📋 Mathlib.FieldTheory.SplittingField.Construction
  (n : ℕ) {K : Type u} [Field K] (f : Polynomial K) (_hfn : f.natDegree = n) : (Polynomial.map (algebraMap K (Polynomial.SplittingFieldAux n f)) f).Splits
• AlgebraicClosure.finEquivRoots 📋 Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
  {k : Type u} [Field k] {K : Type u_1} [Field K] [DecidableEq K] {i : k →+* K} {f : AlgebraicClosure.Monics k} (hf : (Polynomial.map i ↑f).Splits) : Fin (↑f).natDegree ≃ ↥(Polynomial.map i ↑f).roots.toEnumFinset
• AlgebraicClosure.Monics.splits_finsetProd 📋 Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
  {k : Type u} [Field k] {s : Finset (AlgebraicClosure.Monics k)} {f : AlgebraicClosure.Monics k} (hf : f ∈ s) : (Polynomial.map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).Splits
• IntermediateField.splits_of_mem_adjoin 📋 Mathlib.FieldTheory.Normal.Basic
  (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] {S : Set K} (splits : ∀ x ∈ S, IsIntegral F x ∧ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) {x : K} (hx : x ∈ IntermediateField.adjoin F S) : (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
• IsNormalClosure.splits 📋 Mathlib.FieldTheory.Normal.Closure
  {F : Type u_1} {K : Type u_2} {L : Type u_3} {inst✝ : Field F} {inst✝¹ : Field K} {inst✝² : Field L} {inst✝³ : Algebra F K} {inst✝⁴ : Algebra F L} [self : IsNormalClosure F K L] (x : K) : (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
• IsNormalClosure.lift 📋 Mathlib.FieldTheory.Normal.Closure
  {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [h : IsNormalClosure F K L] {L' : Type u_4} [Field L'] [Algebra F L'] (splits : ∀ (x : K), (Polynomial.map (algebraMap F L') (minpoly F x)).Splits) : L →ₐ[F] L'
• Algebra.IsAlgebraic.algHomEmbeddingOfSplits 📋 Mathlib.FieldTheory.Normal.Closure
  {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra.IsAlgebraic F K] (h : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) (L' : Type u_4) [Field L'] [Algebra F L'] : (K →ₐ[F] L') ↪ K →ₐ[F] L
• Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits 📋 Mathlib.FieldTheory.Normal.Closure
  {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra.IsAlgebraic F K] (splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) : IntermediateField.normalClosure F K L = ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L)
• Algebra.IsAlgebraic.isNormalClosure_iff 📋 Mathlib.FieldTheory.Normal.Closure
  {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra.IsAlgebraic F K] : IsNormalClosure F K L ↔ (∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) ∧ IntermediateField.normalClosure F K L = ⊤
• Algebra.IsAlgebraic.isNormalClosure_normalClosure 📋 Mathlib.FieldTheory.Normal.Closure
  {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra.IsAlgebraic F K] (splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) : IsNormalClosure F K ↥(IntermediateField.normalClosure F K L)
• IsNormalClosure.mk 📋 Mathlib.FieldTheory.Normal.Closure
  {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] (splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) (adjoin_rootSet : ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L) = ⊤) : IsNormalClosure F K L
• AlgHom.natCard_of_splits 📋 Mathlib.FieldTheory.PrimitiveElement
  (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable F E] (L : Type u_3) [Field L] [Algebra F L] (hL : ∀ (x : E), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) : Nat.card (E →ₐ[F] L) = Module.finrank F E
• AlgHom.card_of_splits 📋 Mathlib.FieldTheory.PrimitiveElement
  (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable F E] (L : Type u_3) [Field L] [Algebra F L] (hL : ∀ (x : E), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) : Fintype.card (E →ₐ[F] L) = Module.finrank F E
• Field.primitive_element_iff_algHom_eq_of_eval' 📋 Mathlib.FieldTheory.PrimitiveElement
  (F : Type u_3) {E : Type u_4} [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable F E] (A : Type u_5) [Field A] [Algebra F A] (hA : ∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits) (α : E) : F⟮α⟯ = ⊤ ↔ Function.Injective fun φ => φ α
• Field.primitive_element_iff_algHom_eq_of_eval 📋 Mathlib.FieldTheory.PrimitiveElement
  (F : Type u_3) {E : Type u_4} [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable F E] (A : Type u_5) [Field A] [Algebra F A] (hA : ∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits) (α : E) (φ : E →ₐ[F] A) : F⟮α⟯ = ⊤ ↔ ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
• perfectField_iff_splits_of_natSepDegree_eq_one 📋 Mathlib.FieldTheory.SeparableDegree
  (F : Type u_1) [Field F] : PerfectField F ↔ ∀ (f : Polynomial F), f.natSepDegree = 1 → f.Splits
• PerfectField.splits_of_natSepDegree_eq_one 📋 Mathlib.FieldTheory.SeparableDegree
  {E : Type v} [Field E] {K : Type w} [Field K] [PerfectField K] {f : Polynomial E} (i : E →+* K) (hf : f.natSepDegree = 1) : (Polynomial.map i f).Splits
• Polynomial.natSepDegree_eq_of_splits 📋 Mathlib.FieldTheory.SeparableDegree
  {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (f : Polynomial F) [DecidableEq E] (h : (Polynomial.map (algebraMap F E) f).Splits) : f.natSepDegree = (f.aroots E).toFinset.card
• Field.embEquivOfAdjoinSplits 📋 Mathlib.FieldTheory.SeparableDegree
  (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] {S : Set E} (hS : IntermediateField.adjoin F S = ⊤) (hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) : Field.Emb F E ≃ (E →ₐ[F] K)
• Field.finSepDegree_eq_of_adjoin_splits 📋 Mathlib.FieldTheory.SeparableDegree
  (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] {S : Set E} (hS : IntermediateField.adjoin F S = ⊤) (hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) : Field.finSepDegree F E = Nat.card (E →ₐ[F] K)
• Polynomial.Monic.eq_X_sub_C_pow_of_natSepDegree_eq_one_of_splits 📋 Mathlib.FieldTheory.SeparableDegree
  {F : Type u} [Field F] {f : Polynomial F} (hm : f.Monic) (hs : f.Splits) (h : f.natSepDegree = 1) : ∃ m y, m ≠ 0 ∧ f = (Polynomial.X - Polynomial.C y) ^ m

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 23a3216