FLT/HenselianLocalRing/Stuff.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. instance IsIdempotentElem.Corner.algebra line 23 source

   standard axioms: Quot.sound, propext what this means

   Statement uses: CommSemiring, Semiring, Algebra, IsIdempotentElem, IsIdempotentElem.Corner

   Proof uses: Algebra.mk, SMul.mk, Subtype.mk, Membership.mem, Subsemigroup, Subsemigroup.corner, HSMul.hSMul, RingHom.mk, MonoidHom.mk, OneHom.mk

   32 instances, coercions and auxiliary constants left out.

   Tactic trace: 9 steps

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

2. instance (instance at line 40) line 40 source
3. lemma IsIdempotentElem.toCorner_surjective line 45 source

   standard axioms: Quot.sound, propext what this means

   Statement uses: CommSemiring, IsIdempotentElem, Function.Surjective, IsIdempotentElem.Corner, RingHom, Algebra.algebraMap

   Proof uses: Exists.intro, Eq, Membership.mem, Subsemigroup, Subsemigroup.corner, Subtype.ext, And.right, HMul.hMul, Iff.mp, And, Subsemigroup.mem_corner_iff, Subtype.property

   33 instances, coercions and auxiliary constants left out.

4. lemma IsIdempotentElem.ker_toCorner line 50 source

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

   Statement uses: CommRing, IsIdempotentElem, Eq, Ideal, RingHom.ker, IsIdempotentElem.Corner, RingHom, Algebra.algebraMap, Ideal.span, Singleton.singleton, Set, HSub.hSub, OfNat.ofNat

   Proof uses: le_antisymm, Membership.mem, Submodule, Iff.mpr, Dvd.dvd, Ideal.mem_span_singleton, Exists.intro, HMul.hMul, of_eq_true, Eq.trans, True, congrArg, sub_mul, congr, one_mul, mul_comm, id, Subtype, Subsemigroup, Subsemigroup.corner and 10 more

   105 instances, coercions and auxiliary constants left out.

   Tactic trace: 10 steps

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

5. instance (instance at line 60) line 60 source
6. instance (instance at line 65) line 65 source
7. lemma Ideal.isRadical_ker line 71 source

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

   Statement uses: CommRing, IsReduced, RingHom, Ideal.IsRadical, RingHom.ker

   Proof uses: Eq.mpr, Nat, Eq, HPow.hPow, OfNat.ofNat, id, Eq.trans, LE.le, Ideal, Ideal.radical, Membership.mem, Submodule, forall_congr, Exists, implies_congr, congrArg, funext, congrFun', map_pow, eq_zero_of_pow_eq_zero

   38 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

8. lemma Ideal.IsRadical.pow_mem_iff line 76 source

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

   Statement uses: CommRing, Ideal, Ideal.IsRadical, Nat, Ne, OfNat.ofNat, Iff, Membership.mem, HPow.hPow

   Proof uses: Iff.intro, Exists.intro, Ideal.pow_mem_of_mem, Ne.bot_lt

   24 instances, coercions and auxiliary constants left out.

9. lemma Algebra.FormallyUnramified.isField_of_isLocalRing line 81 source

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

   Statement uses: Field, CommRing, Algebra, Algebra.EssFiniteType, Algebra.FormallyUnramified, IsLocalRing, IsField

   Proof uses: Module.Finite, Algebra.FormallyUnramified.finite_of_free, IsArtinianRing, IsArtinianRing.of_finite, IsReduced, Algebra.FormallyUnramified.isReduced_of_field, IsArtinianRing.isField_of_isReduced_of_isLocalRing

   28 instances, coercions and auxiliary constants left out.