NormalRings_normalRing_characterization.lean`

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Mathlib

class NormalDomain line 41 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing
Also declared: APNOutputs/StacksProject/NormalRings_NormalDomain_powerSeries.lean:37 (same declaration text).
class NormalRing line 43 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing
Distinct definitions of this name: APNOutputs/StacksProject/NormalRings_NormalDomain_powerSeries.lean:39 (same statement text; different proof or body). Qualify references as NormalRing@path.
lemma imp13_comaximal line 52 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsReduced, NormalRing, Ideal, Membership.mem, Set, Ideal.minimalPrimes, Bot.bot, Ne, Eq, HAdd.hAdd, Top.top
Proof uses: Classical.byContradiction, Not, And, Ideal.IsMaximal, LE.le, Exists, False, Ideal.exists_le_maximal, le_trans, Max.max, le_sup_left, le_sup_right, Localization.AtPrime, Ideal.IsMaximal.isPrime, NormalDomain, Ideal.primeCompl, NormalRing.localization_atPrime_normalDomain, minimalPrimes, Singleton.singleton, IsDomain.minimalPrimes_eq_singleton_bot and 33 more
91 instances, coercions and auxiliary constants left out.
Tactic trace: 75 steps
Open to load the checked before-and-after goal states.
lemma imp13_iso line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsReduced, Set.Finite, Ideal, Ideal.minimalPrimes, Bot.bot, NormalRing, Nonempty, RingEquiv, Subtype, Membership.mem, Set, HasQuotient.Quotient
Proof uses: Finite, Pairwise, IsCoprime, Ne, Eq, Subtype.ext, HAdd.hAdd, Top.top, imp13_comaximal, Subtype.prop, Iff.mpr, Max.max, Ideal.isCoprime_iff_sup_eq, iInf, InfSet.sInf, Eq.symm, sInf_eq_iInf', Ideal.radical, Ideal.sInf_minimalPrimes, nilradical and 13 more
70 instances, coercions and auxiliary constants left out.
Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma isIntegrallyClosed_of_localization line 152 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDomain, Ideal, Ideal.IsMaximal, IsIntegrallyClosed, Localization.AtPrime, Ideal.primeCompl
Proof uses: IsIntegrallyClosed.of_localization_maximal, Ne, Bot.bot
17 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma NormalDomain_of_NormalRing_and_IsDomain line 158 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDomain, NormalRing, NormalDomain
Proof uses: Ideal, Ideal.IsMaximal, IsIntegrallyClosed, Localization.AtPrime, Ideal.primeCompl, inferInstance, NormalRing.localization_atPrime_normalDomain, NormalDomain.mk, isIntegrallyClosed_of_localization
9 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma isDomain_of_equiv line 166 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, RingEquiv, IsDomain
Proof uses: Eq.mpr, id, Eq, congrArg, propext, MulEquiv.isDomain_iff, RingEquiv.toMulEquiv
18 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma isIntegrallyClosed_of_equiv line 170 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingEquiv, IsIntegrallyClosed
Proof uses: DecidableEq, Classical.decEq, IsIntegrallyClosed.of_equiv, RingEquiv.symm
14 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma normalDomain_of_equiv line 175 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingEquiv, NormalDomain
Proof uses: NormalDomain.mk, isDomain_of_equiv, isIntegrallyClosed_of_equiv
16 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma normalDomain_of_equiv_nonempty line 181 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Nonempty, RingEquiv, NormalDomain
Proof uses: normalDomain_of_equiv
15 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma localRingEquiv_cond line 186 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingEquiv, Ideal, Ideal.IsPrime, Eq, Submonoid, Submonoid.map, MonoidHom, Ideal.primeCompl, Ideal.map
Proof uses: of_eq_true, Submonoid.mk, Subsemigroup.mk, Compl.compl, Set, Ideal.one_notMem, Eq.trans, Iff, Membership.mem, True, forall_congr, Not, congr, congrArg, Exists, And, RingEquiv.symm, funext, Subsemigroup, Eq.symm and 6 more
64 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Localization.localRingEquiv_of_ringEquiv line 191 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingEquiv, Ideal, Ideal.IsPrime, Nonempty, Localization.AtPrime, Ideal.map, Ideal.primeCompl
Proof uses: Nonempty.intro, IsLocalization.ringEquivOfRingEquiv, localRingEquiv_cond
55 instances, coercions and auxiliary constants left out.
lemma NormalRing_of_equiv line 197 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingEquiv, NormalRing
Proof uses: NormalRing.mk, Ideal, Ideal.IsPrime, Ideal.map, NormalDomain, Localization.AtPrime, Ideal.primeCompl, NormalRing.localization_atPrime_normalDomain, Nonempty, Localization.localRingEquiv_of_ringEquiv, normalDomain_of_equiv_nonempty
34 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma prime_prod_equiv line 208 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, CommRing, Ideal, Ideal.IsPrime, Nonempty, RingEquiv, Localization.AtPrime, Ideal.comap, RingHom, Pi.evalRingHom, Ideal.primeCompl
Proof uses: Nonempty.intro, AlgEquiv.toRingEquiv, RingHom.toAlgebra, RingHom.comp, algebraMap, IsLocalization.algEquiv, IsLocalization'.mk, Submonoid.IsLocalizationMap.mk, Subtype, Membership.mem, Submonoid, prime_prod_equiv.match_1, IsUnit, id, Subtype.mk, IsLocalization.map_units, Prod, Eq, HMul.hMul, Prod.snd and 20 more
94 instances, coercions and auxiliary constants left out.
Tactic trace: 54 steps
Open to load the checked before-and-after goal states.
lemma normalRing_factor line 268 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, CommRing, NormalRing
Proof uses: NormalRing.mk, Ideal, Ideal.IsPrime, Ideal.comap, RingHom, Pi.evalRingHom, NormalDomain, Localization.AtPrime, Ideal.comap_isPrime, Ideal.primeCompl, NormalRing.localization_atPrime_normalDomain, Nonempty, RingEquiv, prime_prod_equiv, Nonempty.intro, RingEquiv.symm, normalDomain_of_equiv_nonempty
37 instances, coercions and auxiliary constants left out.
Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma imp13 line 281 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsReduced, Set.Finite, Ideal, Ideal.minimalPrimes, Bot.bot, NormalRing, Exists, Finite, NormalDomain, Nonempty, RingEquiv
Proof uses: Subtype, Membership.mem, Set, Nat, Equiv, Fin, Finite.exists_equiv_fin, HasQuotient.Quotient, imp13_iso, Equiv.symm, RingEquiv.piCongrLeft', RingEquiv.trans, Ideal.IsPrime, And.left, LE.le, And, Subtype.property, normalRing_factor, Fintype.ofFinite, Classical.decEq and 6 more
62 instances, coercions and auxiliary constants left out.
Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma local_idempotent line 305 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Eq, HMul.hMul, Or, OfNat.ofNat
Proof uses: HSub.hSub, Trans.trans, mul_sub, Eq.mpr, id, congrArg, mul_one, Eq.refl, sub_self, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.add_congr, HPow.hPow, Nat, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.sub_congr and 32 more
72 instances, coercions and auxiliary constants left out.
Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma idempotent_of_zero_divisor line 324 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsReduced, IsLocalRing, IsIntegrallyClosed, Eq, HMul.hMul, OfNat.ofNat, Membership.mem, Submonoid, nonZeroDivisors, HAdd.hAdd, Or
Proof uses: FractionRing, RingHom, algebraMap, IsUnit, IsLocalization.map_units, Subtype.mk, Inv.inv, Units, IsUnit.unit, Trans.trans, Eq.mpr, id, congrArg, Eq.symm, map_mul, Eq.refl, add_zero, mul_add, Mathlib.Tactic.Ring.of_eq, HPow.hPow and 67 more
152 instances, coercions and auxiliary constants left out.
Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
lemma exists_x_y_of_min_primes_aux2 line 397 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsReduced, Finset, Ideal, Membership.mem, Ideal.IsPrime, Not, LE.le, Exists, And
Proof uses: HasSubset.Subset, Set, Set.iUnion, Iff.mp, Ideal.subset_union_prime, Ne, False, Set.not_subset, Exists.intro, And.intro, Iff.mpr, Set.mem_iUnion
54 instances, coercions and auxiliary constants left out.
Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma not_prod_le_of_not_le line 416 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, DecidableEq, Ideal, Finset, Ideal.IsPrime, Membership.mem, Not, LE.le, Finset.prod
Proof uses: Exists, And, Eq.mpr, Eq.refl, Iff.mp, Ideal.IsPrime.prod_le, False
34 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma prod_le_of_mem line 423 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, DecidableEq, Ideal, Finset, Membership.mem, LE.le, Finset.prod
Proof uses: Eq, HMul.hMul, Finset.erase, Eq.symm, Finset.mul_prod_erase, Eq.mpr, id, congrArg, Ideal.mul_le_right
39 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma exists_x_y_of_min_primes line 429 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsReduced, Set.Finite, Ideal, Ideal.minimalPrimes, Bot.bot, Membership.mem, Set, Ne, Exists, And, Eq, HMul.hMul, OfNat.ofNat, Submonoid, nonZeroDivisors, HAdd.hAdd, Not
Proof uses: Finset, Finset.filter, Classical.decEq, Set.Finite.toFinset, Ideal.IsPrime, And.left, LE.le, Iff.mp, Set.Finite.mem_toFinset, Finset.mem_filter, And.right, le_antisymm, Eq.symm, exists_x_y_of_min_primes_aux2, Iff.mpr, And.intro, Ne.symm, Finset.prod, not_prod_le_of_not_le, Submodule and 62 more
91 instances, coercions and auxiliary constants left out.
Tactic trace: 99 steps
Open to load the checked before-and-after goal states.
lemma imp23_comaximal line 526 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsReduced, Set.Finite, Ideal, Ideal.minimalPrimes, Bot.bot, IsIntegrallyClosed, Membership.mem, Set, Ne, Eq, HAdd.hAdd, Top.top
Proof uses: Exists, And, HMul.hMul, OfNat.ofNat, Submonoid, nonZeroDivisors, Not, exists_x_y_of_min_primes, FractionRing, RingHom, algebraMap, IsUnit, Subtype.mk, IsLocalization.map_units, Inv.inv, Units, IsUnit.unit, Trans.trans, Eq.mpr, id and 134 more
169 instances, coercions and auxiliary constants left out.
Tactic trace: 86 steps
Open to load the checked before-and-after goal states.
lemma imp23_iso line 610 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsReduced, Set.Finite, Ideal, Ideal.minimalPrimes, Bot.bot, IsIntegrallyClosed, Nonempty, RingEquiv, Subtype, Membership.mem, Set, HasQuotient.Quotient
Proof uses: Finite, Pairwise, IsCoprime, Ne, Eq, Subtype.ext, HAdd.hAdd, Top.top, imp23_comaximal, Subtype.prop, Iff.mpr, Max.max, Ideal.isCoprime_iff_sup_eq, iInf, InfSet.sInf, Eq.symm, sInf_eq_iInf', Ideal.radical, Ideal.sInf_minimalPrimes, nilradical and 13 more
70 instances, coercions and auxiliary constants left out.
Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma eval2_eq_sum_range_deg line 639 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, Polynomial, Nat, LE.le, Polynomial.natDegree, Eq, Polynomial.eval₂, Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, HMul.hMul, Polynomial.coeff, HPow.hPow
Proof uses: Eq.trans, Polynomial.eval₂_eq_sum_range, Finset.sum_subset, GCongr.finset_range_subset_of_le, add_le_add_left, of_eq_true, Membership.mem, Finset, Not, True, forall_congr, implies_congr_ctx, LT.lt, congrArg, Polynomial.coeff_eq_zero_of_natDegree_lt, map_zero, MulZeroClass.zero_mul, eq_self, implies_true
77 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma coeff_sum_monomial line 643 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Nat, LE.le, Eq, Polynomial.coeff, Finset.sum, Polynomial, Finset.range, HAdd.hAdd, OfNat.ofNat, LinearMap, RingHom.id, Polynomial.monomial
Proof uses: of_eq_true, Eq.trans, True, ite, congrArg, Polynomial.finset_sum_coeff, Membership.mem, Finset, Finset.sum_congr, Eq.refl, Polynomial.coeff_monomial, Finset.sum_ite_eq', ite_congr, LT.lt, Nat.succ, propext, Nat.lt_succ_iff, eq_true, True.intro, Not and 1 more
46 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma monic_sum_monomial line 647 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Nat, Eq, OfNat.ofNat, Polynomial.Monic, Finset.sum, Polynomial, Finset.range, HAdd.hAdd, LinearMap, RingHom.id, Polynomial.monomial
Proof uses: Polynomial.monic_of_degree_le, LE.le.trans, WithBot, Polynomial.degree, Finset.sup, Polynomial.degree_sum_le, Finset.sup_le, Function.comp, Membership.mem, Finset, LE.le, Polynomial.degree_monomial_le, cast, Eq.symm, implies_congr, Eq.refl, Iff.mp, Nat.succ, Finset.mem_range_succ_iff, of_eq_true and 12 more
102 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma eval_sum_monomial_pi line 651 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, CommRing, Algebra, Nat, Eq, Polynomial.eval₂, algebraMap, Finset.sum, Polynomial, Finset.range, HAdd.hAdd, OfNat.ofNat, LinearMap, RingHom.id, Polynomial.monomial, HMul.hMul, RingHom, HPow.hPow
Proof uses: Eq.trans, Polynomial.eval₂_finset_sum, funext, Finset.sum_apply, congr_arg, Eq.mpr, id, congrArg, Polynomial.eval₂_monomial, Eq.refl
58 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma isFractionRing_pi line 658 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, CommRing, IsDomain, IsFractionRing, FractionRing, nonZeroDivisors
Proof uses: Exists.elim, Rat, Eq, OfNat.ofNat, HMul.hMul, HAdd.hAdd, Eq.dvd, Rat.add_zero, IsLocalization'.mk, Submonoid.IsLocalizationMap.mk, RingHom, algebraMap, Eq.mpr, Subtype, Membership.mem, Submonoid, IsUnit, Not, id, Eq.trans and 57 more
126 instances, coercions and auxiliary constants left out.
Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma isIntegrallyClosed_factor_aux1 line 674 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, CommRing, IsDomain, FractionRing, Polynomial, Polynomial.Monic, Finset.sum, Nat, Finset.range, HAdd.hAdd, Polynomial.natDegree, OfNat.ofNat, LinearMap, RingHom.id, Polynomial.monomial, dite, Eq, Eq.rec, Polynomial.coeff and 3 more
Proof uses: Polynomial.monic_of_degree_le, LE.le.trans, WithBot, Polynomial.degree, Finset.sup, Polynomial.degree_sum_le, Finset.sup_le, Function.comp, Membership.mem, Finset, LE.le, Polynomial.degree_monomial_le, cast, implies_congr, Eq.refl, Iff.mp, Nat.succ, Finset.mem_range_succ_iff, funext, Eq.mpr and 21 more
99 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma isIntegrallyClosed_factor_aux2_p_eq_1 line 682 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDomain, Polynomial, Polynomial.Monic, Eq, Nat, Polynomial.natDegree, OfNat.ofNat
Proof uses: Iff.mp, Polynomial.Monic.natDegree_eq_zero
10 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma isIntegrallyClosed_factor_aux2_sum_zero line 684 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, CommRing, IsDomain, Polynomial, FractionRing, Not, Eq, LT.lt, Nat, OfNat.ofNat, Polynomial.natDegree, Finset.sum, nonZeroDivisors, Finset.range, HAdd.hAdd, HMul.hMul, RingHom, algebraMap, dite and 5 more
Proof uses: of_eq_true, Eq.trans, True, congrArg, Membership.mem, Finset, Finset.sum_congr, Eq.refl, False, Eq.mpr_prop, eq_false, not_false, congr, dite_congr, MonoidWithZeroHom.map_ite_one_zero, ite_mul, ite_congr, one_mul, MulZeroClass.zero_mul, Finset.sum_ite_eq' and 11 more
127 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma isIntegrallyClosed_factor_aux2 line 689 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, CommRing, IsDomain, FractionRing, Polynomial, Polynomial.Monic, Eq, Polynomial.eval₂, nonZeroDivisors, algebraMap, OfNat.ofNat, dite, Eq.rec, Eq.symm, Not, Finset.sum, Nat, Finset.range, HAdd.hAdd and 6 more
Proof uses: HMul.hMul, RingHom, HPow.hPow, eval_sum_monomial_pi, Eq.mpr, id, congrArg, funext, Finset.sum_congr, rfl, Finset, Membership.mem, of_eq_true, Eq.trans, True, ite_cond_eq_true, eq_self, Eq.refl, eval2_eq_sum_range_deg, le_refl and 16 more
124 instances, coercions and auxiliary constants left out.
Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
lemma isIntegrallyClosed_factor line 735 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, CommRing, IsDomain, IsIntegrallyClosed
Proof uses: FractionRing, IsIntegral, nonZeroDivisors, Exists, Eq, RingHom, algebraMap, Iff.mp, isIntegrallyClosed_iff, isFractionRing_pi, Eq.mpr, id, congrArg, propext, Polynomial, And, Polynomial.Monic, Polynomial.eval₂, OfNat.ofNat, Nat and 21 more
53 instances, coercions and auxiliary constants left out.
Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma imp23 line 759 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsReduced, Set.Finite, Ideal, Ideal.minimalPrimes, Bot.bot, IsIntegrallyClosed, Exists, Finite, NormalDomain, Nonempty, RingEquiv
Proof uses: Subtype, Membership.mem, Set, Nat, Equiv, Fin, Finite.exists_equiv_fin, HasQuotient.Quotient, imp23_iso, Equiv.symm, RingEquiv.piCongrLeft', RingEquiv.trans, isIntegrallyClosed_of_equiv, RingEquiv.symm, Ideal.IsPrime, And.left, LE.le, And, Subtype.property, IsDomain and 7 more
63 instances, coercions and auxiliary constants left out.
Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma eval2_comm_pi line 789 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finite, CommRing, Algebra, Polynomial, Eq, Polynomial.eval₂, algebraMap, Polynomial.map, Pi.evalRingHom
Proof uses: Eq.mpr, Finset.sum, Nat, Finset.range, HAdd.hAdd, Polynomial.natDegree, OfNat.ofNat, HMul.hMul, RingHom, Polynomial.coeff, HPow.hPow, id, congr, congrArg, Eq.trans, congrFun, Polynomial.eval₂_eq_sum_range, Finset.sum_apply, Finset.sum_congr, Eq.refl and 29 more
51 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma isIntegrallyClosed_pi_eval_zero line 797 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finite, CommRing, Algebra, Polynomial, Eq, Polynomial.eval₂, algebraMap, OfNat.ofNat, Polynomial.map, Pi.evalRingHom
Proof uses: Eq.mpr, id, congrArg, Eq.refl, eval2_comm_pi, Eq.symm
28 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma isIntegrallyClosed_pi line 808 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finite, CommRing, NormalDomain, IsIntegrallyClosed
Proof uses: IsFractionRing, FractionRing, nonZeroDivisors, isFractionRing_pi, Fintype.ofFinite, Classical.decEq, inferInstance, IsDomain, Eq.mpr, IsIntegral, Exists, Eq, RingHom, algebraMap, id, congrArg, propext, isIntegrallyClosed_iff, Polynomial, And and 13 more
32 instances, coercions and auxiliary constants left out.
Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma imp32 line 832 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsReduced, Set.Finite, Ideal, Ideal.minimalPrimes, Bot.bot, Exists, Finite, NormalDomain, Nonempty, RingEquiv, IsIntegrallyClosed
Proof uses: isIntegrallyClosed_of_equiv, inferInstance, isIntegrallyClosed_pi
45 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma pi_prime_idempotent line 841 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, CommRing, Ideal, Ideal.IsPrime, Exists, Not, Membership.mem, ite, Eq, OfNat.ofNat
Proof uses: Classical.byContradiction, Finset.sum, Finset.univ, Ideal.sum_mem, Finset, Eq.mp, Eq.trans, binderNameHint, forall_congr, funext, Eq.mpr, id, congrArg, Finset.sum_apply, Finset.sum_eq_single, Ne, of_eq_true, True, ite_cond_eq_false, eq_false and 14 more
69 instances, coercions and auxiliary constants left out.
Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
def loc_equiv_of_eq line 864 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal, Ideal.IsPrime, Eq, RingEquiv, Localization.AtPrime, Ideal.primeCompl
Proof uses: RingEquiv.refl
39 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma pi_localization_equiv line 869 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, CommRing, Ideal, Ideal.IsPrime, Not, Membership.mem, ite, Eq, OfNat.ofNat, Ideal.map, RingHom, Pi.evalRingHom, Nonempty, RingEquiv, Localization.AtPrime, Ideal.primeCompl
Proof uses: Function.Surjective, Exists.intro, dite, Eq.rec, dif_pos, rfl, Ideal.comap, Ideal.ext, Iff.intro, And, Exists, Iff.mp, Ideal.mem_map_iff_of_surjective, HMul.hMul, HSub.hSub, funext, of_eq_true, Eq.trans, True, congrArg and 30 more
121 instances, coercions and auxiliary constants left out.
Tactic trace: 56 steps
Open to load the checked before-and-after goal states.
lemma normalDomain_of_localization line 925 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, NormalDomain, Ideal, Ideal.IsPrime, Localization.AtPrime, Ideal.primeCompl
Proof uses: LE.le, Submonoid, nonZeroDivisors, Membership.mem, Ne, OfNat.ofNat, Eq, Eq.mp, congrArg, Ideal.zero_mem, Iff.mpr, mem_nonZeroDivisors_iff_ne_zero, NormalDomain.mk, IsLocalization.isDomain_localization, isIntegrallyClosed_of_isLocalization
37 instances, coercions and auxiliary constants left out.
Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma pi_ideal_map_prime line 938 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, CommRing, Ideal, Ideal.IsPrime, Not, Membership.mem, ite, Eq, OfNat.ofNat, Ideal.map, RingHom, Pi.evalRingHom
Proof uses: HMul.hMul, HSub.hSub, funext, dite, id, dif_pos, rfl, Eq.mpr, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.mul_congr, HAdd.hAdd, Nat.rawCast, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.sub_pf, Int.rawCast, Int.negOfNat and 47 more
77 instances, coercions and auxiliary constants left out.
Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
lemma normalRing_of_pi line 980 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, CommRing, NormalDomain, NormalRing
Proof uses: NormalRing.mk, Ideal, Ideal.IsPrime, Exists, Not, Membership.mem, ite, Eq, OfNat.ofNat, pi_prime_idempotent, Localization.AtPrime, Ideal.primeCompl, Ideal.map, RingHom, Pi.evalRingHom, Nonempty, RingEquiv, pi_ideal_map_prime, pi_localization_equiv, normalDomain_of_localization and 1 more
43 instances, coercions and auxiliary constants left out.
Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma imp31 line 993 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsReduced, Set.Finite, Ideal, Ideal.minimalPrimes, Bot.bot, Exists, Finite, NormalDomain, Nonempty, RingEquiv, NormalRing
Proof uses: normalRing_of_pi, Fintype.ofFinite, Classical.decEq, NormalRing_of_equiv
45 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma main_lemma line 1004 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsReduced, Set.Finite, Ideal, Ideal.minimalPrimes, Bot.bot, List.TFAE, List.cons, NormalRing, IsIntegrallyClosed, Exists, Finite, NormalDomain, Nonempty, RingEquiv, List.nil
Proof uses: imp13, imp31, imp32, imp23, List.tfae_of_cycle, List.IsChain.cons_cons, List.IsChain.singleton
42 instances, coercions and auxiliary constants left out.
Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
theorem normalRing_characterization line 1029 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsReduced, Set.Finite, Ideal, Ideal.minimalPrimes, Bot.bot, List.TFAE, List.cons, NormalRing, IsIntegrallyClosed, Exists, Finite, NormalDomain, Nonempty, RingEquiv, List.nil
Proof uses: main_lemma
37 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.