FLT/Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma Polynomial.IsSplittingField.finrank_le_factorial_aux line 16 source

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

   Statement uses: Field, Algebra, Polynomial, Polynomial.IsSplittingField, LE.le, Nat, Module.finrank, Nat.factorial, Polynomial.natDegree

   Proof uses: Nat.recAux, Eq, OfNat.ofNat, RingHom, Polynomial.C, Exists, Iff.mp, Polynomial.natDegree_eq_zero, Eq.mp, Subalgebra, Algebra.adjoin, Polynomial.rootSet, Top.top, Eq.trans, Bot.bot, congrFun', congrArg, EmptyCollection.emptyCollection, Set, Polynomial.rootSet_C and 110 more

   158 instances, coercions and auxiliary constants left out.

   Tactic trace: 52 steps

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

2. lemma Polynomial.IsSplittingField.finrank_le_factorial line 65 source

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

   Statement uses: Field, Algebra, Polynomial, Polynomial.IsSplittingField, LE.le, Nat, Module.finrank, Nat.factorial, Polynomial.natDegree

   Proof uses: Eq.mp, Subtype, Membership.mem, IntermediateField, Bot.bot, Polynomial.map, Algebra.algebraMap, congr, congrArg, IntermediateField.finrank_bot', Polynomial.natDegree_map, Polynomial.IsSplittingField.finrank_le_factorial_aux

   52 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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