FLT/HenselianLocalRing/Finite.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma Ideal.isMaximal_of_isMaximal_under_of_formallyUnramified line 34 source
2. instance (instance at line 54) line 54 source
3. lemma HenselianLocalRing.exists_lift_of_to_ResidueField line 61 source
4. lemma HenselianLocalRing.exists_completeOrthogonalIdempotents_forall_isLocalRing line 96 source
5. lemma Ideal.quotientKerAlgEquivOfSurjective_symm_apply' line 180 source
6. lemma Module.finrank_pos_of_free line 186 source
7. lemma Module.finrank_eq_one_iff_algebraMap_bijective line 191 source
8. theorem HenselianLocalRing.of_finite_aux line 203 source
9. lemma HenselianLocalRing.of_finite line 245 source

   depends on sorry (Lean reported 1 error(s) in this file) what this means

   Statement uses: CommRing, HenselianLocalRing, Algebra, Module.Finite, IsLocalRing

   Proof uses: HenselianLocalRing.mk, Polynomial, Polynomial.Monic, Membership.mem, Ideal, IsLocalRing.maximalIdeal, Polynomial.eval, IsUnit, LinearMap, RingHom.id, Polynomial.derivative, AdjoinRoot, Polynomial.Monic.finite_adjoinRoot, Module.Free, Polynomial.Monic.free_adjoinRoot, Module.Finite.trans, Nat, Exists, Fin, CompleteOrthogonalIdempotents and 128 more

   146 instances, coercions and auxiliary constants left out.

   Tactic trace: 61 steps

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

10. instance (instance at line 302) line 302 source
11. lemma HenselianLocalRing.exist_residueFieldMap_eq_of_etale line 314 source

    depends on sorry (Lean reported 1 error(s) in this file) what this means

    Statement uses: CommRing, HenselianLocalRing, IsLocalRing, Algebra, IsLocalHom, RingHom, Algebra.algebraMap, Algebra.Etale, Module.Finite, AlgHom, IsLocalRing.ResidueField, Exists, AlgHom.toRingHom, Eq, IsLocalRing.ResidueField.map

    Proof uses: HenselianLocalRing.of_finite, TensorProduct, Algebra.TensorProduct.lift, Algebra.ofId, AlgHom.comp, AlgHom.restrictScalars, IsScalarTower.toAlgHom, Commute.all, HenselianLocalRing.exists_lift_of_to_ResidueField, Algebra.TensorProduct.includeRight, IsLocalRing.residue, Trans.simple, TensorProduct.tmul, OfNat.ofNat, Eq.symm, id, congrArg, of_eq_true, Eq.trans, True and 20 more

    98 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

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

12. lemma IsLocalRing.eq_of_eval_derivative_notMem line 339 source
13. lemma HenselianLocalRing.eq_of_toAlgHom_residueField_comp_eq_of_isStandardEtale line 357 source
14. lemma HenselianLocalRing.eq_of_toAlgHom_residueField_comp_eq line 371 source
15. lemma HenselianLocalRing.eq_of_residueFieldMap_eq line 395 source

    depends on sorry (Lean reported 1 error(s) in this file) what this means

    Statement uses: CommRing, HenselianLocalRing, IsLocalRing, Algebra, Algebra.Etale, Module.Finite, AlgHom, IsLocalHom, RingHom, AlgHom.toRingHom, Eq, IsLocalRing.ResidueField, IsLocalRing.ResidueField.map

    Proof uses: HenselianLocalRing.of_finite, TensorProduct, Algebra.TensorProduct.lift, Algebra.ofId, Commute.all, HenselianLocalRing.eq_of_toAlgHom_residueField_comp_eq, Algebra.TensorProduct.ext_ring, AlgHom.comp, IsScalarTower.toAlgHom, AlgHom.ext, AlgHom.restrictScalars, Algebra.TensorProduct.includeRight, Eq.mpr, IsLocalRing.residue, id, congr, congrArg, AlgHom.id, Commute, Eq.refl and 5 more

    54 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

16. lemma HenselianLocalRing.exist_algEquiv_residueFieldMap_eq_of_etale line 410 source

    depends on sorry (Lean reported 1 error(s) in this file) what this means

    Statement uses: CommRing, HenselianLocalRing, IsLocalRing, Algebra, Module.Finite, Algebra.Etale, AlgEquiv, IsLocalRing.ResidueField, Exists, IsLocalHom, RingHom, RingEquiv.toRingHom, AlgEquiv.toRingEquiv, Eq, IsLocalRing.ResidueField.map

    Proof uses: AlgHom, AlgHom.toRingHom, HenselianLocalRing.exist_residueFieldMap_eq_of_etale, AlgEquiv.symm, AlgHom.comp, AlgHom.id, id, inferInstance, RingHom.id, HenselianLocalRing.eq_of_residueFieldMap_eq, Eq.mpr, RingHom.comp, congr, congrArg, Eq.trans, IsLocalRing.ResidueField.map_comp, IsLocalRing.ResidueField.map_id, RingHom.ext, of_eq_true, True and 6 more

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 27 steps

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