FLT/Mathlib/RingTheory/AdjoinRoot.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem AdjoinRoot.map_comp_mk Reduction along f : A →+* B descends to AdjoinRoot: the square A[X] → B[X] → B[X]/(q) = A[X] → A[X]/(p) → B[X]/(q) commutes when q = p.map f line 25 source

   Source documentation

   Reduction along f : A →+* B descends to AdjoinRoot: the square A[X] → B[X] → B[X]/(q) = A[X] → A[X]/(p) → B[X]/(q) commutes when q = p.map f.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: CommRing, RingHom, Polynomial, Eq, Polynomial.map, AdjoinRoot, RingHom.comp, AdjoinRoot.map, Eq.dvd, AdjoinRoot.mk, Polynomial.mapRingHom

   Proof uses: Polynomial.ringHom_ext, Eq.mpr, Polynomial.C, id, congrArg, RingHom.comp_apply, AdjoinRoot.of, AdjoinRoot.mk_C, AdjoinRoot.map_of, Polynomial.coe_mapRingHom, Polynomial.map_C, Eq.refl, Polynomial.X, AdjoinRoot.root, Eq.symm, AdjoinRoot.root.eq_1, AdjoinRoot.map_root, Polynomial.map_X

   14 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

   Open to load the checked before-and-after goal states.

   theorem AdjoinRoot.map_comp_mk {A B : Type*} [CommRing A] [CommRing B] (f : A →+* B) {p : A[X]}
       {q : B[X]} (h : q = p.map f) :
       (map f p q h.dvd).comp (mk p)
         = (mk q).comp (Polynomial.mapRingHom f) := by
   …

2. theorem AdjoinRoot.finrank_eq_natDegree The simple extension F[X]/(q) by a root of an irreducible q has degree natDegree q line 37 source

   Source documentation

   The simple extension F[X]/(q) by a root of an irreducible q has degree natDegree q.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, Polynomial, Fact, Irreducible, Eq, Nat, Module.finrank, AdjoinRoot, Polynomial.natDegree

   Proof uses: Eq.mpr, PowerBasis.dim, AdjoinRoot.powerBasis, Irreducible.ne_zero, Fact.out, id, congrArg, PowerBasis.finrank, AdjoinRoot.powerBasis_dim, Eq.refl

   30 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem AdjoinRoot.finrank_eq_natDegree {F : Type*} [Field F] {q : F[X]}
       [Fact (Irreducible q)] : Module.finrank F (AdjoinRoot q) = q.natDegree := by
   …

3. theorem AdjoinRoot.natDegree_minpoly_root The minimal polynomial of root q has the same degree as the irreducible q line 45 source

   Source documentation

   The minimal polynomial of root q has the same degree as the irreducible q.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, Polynomial, Fact, Irreducible, Eq, Nat, Polynomial.natDegree, minpoly, AdjoinRoot, AdjoinRoot.root

   Proof uses: Ne, OfNat.ofNat, Irreducible.ne_zero, Fact.out, Eq.mpr, HMul.hMul, RingHom, Polynomial.C, Inv.inv, Polynomial.leadingCoeff, id, congrArg, AdjoinRoot.minpoly_root, HAdd.hAdd, Polynomial.natDegree_mul, Iff.mpr, Polynomial.C_ne_zero, inv_ne_zero, Polynomial.leadingCoeff_ne_zero, Polynomial.natDegree_C and 2 more

   56 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

   Open to load the checked before-and-after goal states.

   theorem AdjoinRoot.natDegree_minpoly_root {F : Type*} [Field F] {q : F[X]}
       [Fact (Irreducible q)] : (minpoly F (root q)).natDegree = q.natDegree := by
   …

4. theorem AdjoinRoot.eq_zero_of_mul_root_add_eq_zero Documented declaration: eq_zero_of_mul_root_add_eq_zero line 53 source

   Source documentation

   In F[X]/(q) with q irreducible of degree at least 2, the elements 1 and root q are linearly independent over F: a linear relation a · root q + b = 0 forces a = b = 0.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, Polynomial, Fact, Irreducible, LE.le, Nat, OfNat.ofNat, Polynomial.natDegree, Eq, AdjoinRoot, HAdd.hAdd, HMul.hMul, RingHom, Algebra.algebraMap, AdjoinRoot.root, And

   Proof uses: AlgHom, Polynomial.aeval, Polynomial.C, Polynomial.X, Eq.mpr, id, congrFun', congrArg, Eq.trans, map_add, RingHom.id, congr, map_mul, MonoidHom.id, Polynomial.aeval_C, Polynomial.aeval_X, Classical.byContradiction, Not, minpoly, Polynomial.natDegree_le_of_dvd and 19 more

   85 instances, coercions and auxiliary constants left out.

   Tactic trace: 11 steps

   Open to load the checked before-and-after goal states.

   theorem AdjoinRoot.eq_zero_of_mul_root_add_eq_zero {F : Type*} [Field F] {q : F[X]}
       [Fact (Irreducible q)] (hdeg : 2 ≤ q.natDegree) {a b : F}
       (hab : algebraMap F (AdjoinRoot q) a * root q
         + algebraMap F (AdjoinRoot q) b = 0) : a = 0 ∧ b = 0 := by
   …

5. theorem AdjoinRoot.root_notMem_range_algebraMap The root of an irreducible polynomial of degree at least 2 does not lie in the base field line 69 source

   Source documentation

   The root of an irreducible polynomial of degree at least 2 does not lie in the base field.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, Polynomial, Fact, Irreducible, LE.le, Nat, OfNat.ofNat, Polynomial.natDegree, Not, Membership.mem, AdjoinRoot, Set, Set.range, RingHom, Algebra.algebraMap, AdjoinRoot.root

   Proof uses: Eq, False, minpoly, AdjoinRoot.natDegree_minpoly_root, Eq.mp, HSub.hSub, Polynomial.X, Polynomial.C, congrArg, Polynomial.natDegree_X_sub_C, minpoly.eq_X_sub_C, Eq.symm

   42 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

   Open to load the checked before-and-after goal states.

   theorem AdjoinRoot.root_notMem_range_algebraMap {F : Type*} [Field F] {q : F[X]}
       [Fact (Irreducible q)] (hdeg : 2 ≤ q.natDegree) :
       root q ∉ Set.range (algebraMap F (AdjoinRoot q)) := by
   …