IntegralClosure.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

24 declarations, 0 contain sorry, 0 declared as axioms

The general "AKLB" set-up. K is the field of fractions of the Dedekind domain A, L/K is a finite separable extension, and B is the integral closure of A in L.

Imports (7)

Imported by 4 files

def IsDedekindDomain.HeightOneSpectrum.Extension Documented declaration: Extension line 41 source
Source documentation
If B is an A-algebra and v : HeightOneSpectrum A is a nonzero prime, then v.Extension B is the subtype of HeightOneSpeectrum B consisting of valuations of B which restrict to v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, IsDedekindDomain, Algebra.IsIntegral, IsDedekindDomain.HeightOneSpectrum
Proof uses: Subtype, Eq, IsDedekindDomain.HeightOneSpectrum.under
7 instances, coercions and auxiliary constants left out.
```
def Extension (v : HeightOneSpectrum A) := {w : HeightOneSpectrum B // w.under A = v}
```
lemma IsDedekindDomain.HeightOneSpectrum.mk_count_factors_map line 43 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, IsDedekindDomain, Algebra.IsIntegral, Function.Injective, RingHom, Algebra.algebraMap, IsDedekindDomain.HeightOneSpectrum, Ideal, Eq, Nat, Associates.count, Associates.mk, IsDedekindDomain.HeightOneSpectrum.asIdeal, Associates.factors, Ideal.map, HMul.hMul, Ideal.ramificationIdx, IsDedekindDomain.HeightOneSpectrum.under
Proof uses: UniqueFactorizationMonoid.induction_on_prime, Eq.mpr, OfNat.ofNat, Associates, id, congrArg, Associates.mk_zero, Bot.bot, Ideal.zero_eq_bot, Ideal.map_bot, Eq.symm, of_eq_true, Eq.trans, True, congr, dite, Associates.FactorSet, Irreducible, Associates.bcount, Subtype.mk and 71 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.HeightOneSpectrum.ramificationIdx_ne_zero line 91 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, IsDedekindDomain, Algebra.IsIntegral, Function.Injective, RingHom, Algebra.algebraMap, IsDedekindDomain.HeightOneSpectrum, Ne, Nat, Ideal.ramificationIdx, IsDedekindDomain.HeightOneSpectrum.asIdeal, OfNat.ofNat
Proof uses: Ideal, Ideal.map, IsDedekindDomain.HeightOneSpectrum.under, Bot.bot, Iff.mpr, Not, Eq, Iff.not, Ideal.map_eq_bot_iff_of_injective, IsDedekindDomain.HeightOneSpectrum.ne_bot, Eq.mpr, Ideal.ramificationIdx', id, congrArg, Eq.symm, Ideal.ramificationIdx'_eq_ramificationIdx', Ideal.IsDedekindDomain.ramificationIdx'_ne_zero, Ideal.map_comap_le
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.HeightOneSpectrum.intValuation_comap If w | v then for a ∈ A we have w(a)=v(a)^e where e is the ramification index line 100 source
Source documentation
If w | v then for a ∈ A we have w(a)=v(a)^e where e is the ramification index.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, IsDedekindDomain, Algebra.IsIntegral, Function.Injective, RingHom, Algebra.algebraMap, IsDedekindDomain.HeightOneSpectrum, Eq, WithZero, Multiplicative, Int, HPow.hPow, Nat, Valuation, IsDedekindDomain.HeightOneSpectrum.intValuation, IsDedekindDomain.HeightOneSpectrum.under, Ideal.ramificationIdx, IsDedekindDomain.HeightOneSpectrum.asIdeal
Proof uses: Ne, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.ramificationIdx_ne_zero, dite, Classical.propDecidable, Eq.mpr, Not, id, Eq.trans, And, congr, congrArg, congrFun', map_zero, True, eq_self, true_and, IsDedekindDomain.HeightOneSpectrum.intValuationDef, ite, WithZero.exp and 34 more
138 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma intValuation_comap (hAB : Function.Injective (algebraMap A B))
    (w : HeightOneSpectrum B) (x : A) :
    (under A w).intValuation x ^ w.asIdeal.ramificationIdx A =
    w.intValuation (algebraMap A B x) := by
…
```
lemma IsDedekindDomain.HeightOneSpectrum.valuation_comap If w | v then for x ∈ K we have w(x)=v(x)^e where e is the ramification index line 117 source
Source documentation
If w | v then for x ∈ K we have w(x)=v(x)^e where e is the ramification index.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, IsDedekindDomain.HeightOneSpectrum, Eq, WithZero, Multiplicative, Int, HPow.hPow, Nat, Valuation, IsDedekindDomain.HeightOneSpectrum.valuation, IsDedekindDomain.HeightOneSpectrum.under, Ideal.ramificationIdx, IsDedekindDomain.HeightOneSpectrum.asIdeal, RingHom and 1 more
Proof uses: Exists, And, Membership.mem, Submonoid, nonZeroDivisors, HDiv.hDiv, IsFractionRing.div_surjective, of_eq_true, Eq.trans, IsDedekindDomain.HeightOneSpectrum.intValuation, True, congr, congrArg, congrFun', map_div₀, Valuation.extendToLocalization, Set.mem_compl, Ideal, Valuation.supp, IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero' and 9 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma valuation_comap (w : HeightOneSpectrum B) (x : K) :
    (under A w).valuation K x ^ w.asIdeal.ramificationIdx A =
    w.valuation L (algebraMap K L x) := by
…
```
lemma IsDedekindDomain.HeightOneSpectrum.isTorsionFree line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsScalarTower, IsDomain, Module.IsTorsionFree
Proof uses: FaithfulSMul, FaithfulSMul.of_field_isFractionRing, Nontrivial, Iff.mpr, IsFractionRing.nontrivial_iff_nontrivial, inferInstance
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem IsDedekindDomain.HeightOneSpectrum.Extension.finite There are only finitely many nonzero primes of B above a nonzero prime of A line 135 source
Source documentation
There are only finitely many nonzero primes of B above a nonzero prime of A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, IsDedekindDomain.HeightOneSpectrum, Finite, IsDedekindDomain.HeightOneSpectrum.Extension
Proof uses: Module.IsTorsionFree, IsDedekindDomain.HeightOneSpectrum.isTorsionFree, Eq.mpr, Subtype, Eq, IsDedekindDomain.HeightOneSpectrum.under, id, congrArg, IsDedekindDomain.HeightOneSpectrum.Extension.eq_1, Set.ofPred, Eq.symm, Set.coe_ofPred, Set.Finite, propext, Set.finite_coe_iff, Ideal, Ideal.primesOver, IsDedekindDomain.HeightOneSpectrum.asIdeal, IsDedekindDomain.primesOver_finite, Set.Finite.of_finite_image and 24 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem Extension.finite (v : HeightOneSpectrum A) : Finite (v.Extension B) := by
…
```
def IsDedekindDomain.HeightOneSpectrum.Extension.fintype There are only finitely many nonzero primes of B above a nonzero prime of A line 153 source
Source documentation
There are only finitely many nonzero primes of B above a nonzero prime of A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, IsDedekindDomain.HeightOneSpectrum, Fintype, IsDedekindDomain.HeightOneSpectrum.Extension
Proof uses: Finite, IsDedekindDomain.HeightOneSpectrum.Extension.finite, Fintype.ofFinite
12 instances, coercions and auxiliary constants left out.
```
noncomputable def Extension.fintype : Fintype (Extension B v) :=
…
```
Mentions: IsDedekindDomain.HeightOneSpectrum.Extension
theorem IsDedekindDomain.HeightOneSpectrum.preimage_comap_finite line 159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, Set, IsDedekindDomain.HeightOneSpectrum, Set.Finite, Set.preimage, IsDedekindDomain.HeightOneSpectrum.under
Proof uses: Eq.mpr, Set.iUnion, Membership.mem, Singleton.singleton, id, Eq, congrArg, Eq.symm, Set.biUnion_preimage_singleton, Set.Finite.biUnion', IsDedekindDomain.HeightOneSpectrum.Extension.finite
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def IsDedekindDomain.HeightOneSpectrum.preimageComapFinset Given an inclusion of Dedekind domains A → B, making B finite over A, this is the preimage of a Finset of finite places of A, as a Finset of finite places of B line 167 source
Source documentation
Given an inclusion of Dedekind domains A → B, making B finite over A, this is the preimage of a Finset of finite places of A, as a Finset of finite places of B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, Finset, IsDedekindDomain.HeightOneSpectrum
Proof uses: Set.Finite.toFinset, Set.preimage, IsDedekindDomain.HeightOneSpectrum.under
16 instances, coercions and auxiliary constants left out.
```
noncomputable def preimageComapFinset (S : Finset (HeightOneSpectrum A)) :
    Finset (HeightOneSpectrum B) :=
…
```
def IsDedekindDomain.HeightOneSpectrum.Extension.equivPrimesOver The primes of B extending v are precisely the primes of B lying over v.asIdeal line 173 source
Source documentation
The primes of B extending v are precisely the primes of B lying over v.asIdeal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, IsDedekindDomain.HeightOneSpectrum, Equiv, IsDedekindDomain.HeightOneSpectrum.Extension, Ideal, Ideal.primesOver, IsDedekindDomain.HeightOneSpectrum.asIdeal
Proof uses: Module.IsTorsionFree, Equiv.mk, Subtype.mk, Membership.mem, Set, Eq, IsDedekindDomain.HeightOneSpectrum.under, IsDedekindDomain.HeightOneSpectrum.mk
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
noncomputable def Extension.equivPrimesOver : Extension B v ≃ v.asIdeal.primesOver B :=
…
```
Mentions: IsDedekindDomain.HeightOneSpectrum.Extension
lemma IsDedekindDomain.HeightOneSpectrum.Extension.equivPrimesOver_apply line 183 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, Algebra.IsIntegral, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.Extension, Eq, Ideal, Membership.mem, Set, Ideal.primesOver, IsDedekindDomain.HeightOneSpectrum.asIdeal, Equiv, IsDedekindDomain.HeightOneSpectrum.Extension.equivPrimesOver, IsDedekindDomain.HeightOneSpectrum.under
Proof uses: rfl
25 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.HeightOneSpectrum._root_.Ideal.sum_ramification_inertia_extensions Ideal.sum_ramification_inertia_eq_finrank, rewritten as a sum over extensions line 189 source
Source documentation
Ideal.sum_ramification_inertia_eq_finrank, rewritten as a sum over extensions.
```
lemma _root_.Ideal.sum_ramification_inertia_extensions [Module.Finite A B] :
    letI := Extension.fintype A K L B v
…
```
Mentions: IsDedekindDomain.HeightOneSpectrum.Extension.fintype
def IsDedekindDomain.LinearEquivTensorProduct The canonical K-linear isomorphism L ≅ K ⊗ B line 215 source
Source documentation
The canonical K-linear isomorphism L ≅ K ⊗ B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, IsIntegralClosure, Algebra.IsAlgebraic, LinearEquiv, RingHom.id, TensorProduct
Proof uses: Localization, nonZeroDivisors, LocalizedModule, LocalizedModule.equivTensorProduct, IsLocalization, Algebra.algebraMapSubmonoid, IsLocalizedModule, AlgHom.toLinearMap, IsScalarTower.toAlgHom, IsLocalizedModule.iso, AlgHom, TensorProduct.congr, Localization.algEquiv, LinearEquiv.refl, LinearEquiv.extendScalarsOfIsLocalization, LinearEquiv.trans, LinearEquiv.symm, LinearEquiv.restrictScalars
58 instances, coercions and auxiliary constants left out.
```
noncomputable def LinearEquivTensorProduct :
    L ≃ₗ[K] K ⊗[A] B :=
…
```
lemma IsDedekindDomain.LinearEquivTensorProduct_symm_one_tmul line 228 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, IsIntegralClosure, Algebra.IsAlgebraic, Eq, LinearEquiv, RingHom.id, TensorProduct, LinearEquiv.symm, IsDedekindDomain.LinearEquivTensorProduct, TensorProduct.tmul, OfNat.ofNat, RingHom, Algebra.algebraMap
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, LinearEquiv.extendScalarsOfIsLocalization, nonZeroDivisors, LinearEquiv.trans, Localization, LocalizedModule, IsLocalizedModule.iso, AlgHom, IsScalarTower.toAlgHom, LinearEquiv.restrictScalars, LocalizedModule.equivTensorProduct, TensorProduct.congr, Localization.algEquiv, LinearEquiv.refl, LinearMap, LinearEquiv.extendScalarsOfIsLocalization_symm_apply and 14 more
100 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.LinearEquivTensorProduct_symm_tmul line 232 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, IsIntegralClosure, Algebra.IsAlgebraic, Eq, LinearEquiv, RingHom.id, TensorProduct, LinearEquiv.symm, IsDedekindDomain.LinearEquivTensorProduct, TensorProduct.tmul, HSMul.hSMul, RingHom, Algebra.algebraMap
Proof uses: OfNat.ofNat, of_eq_true, Eq.trans, True, congrArg, congrFun', mul_one, eq_self, Eq.mpr, id, LinearEquiv.map_smul, IsDedekindDomain.LinearEquivTensorProduct_symm_one_tmul, Eq.refl
59 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def IsDedekindDomain.linearEquivTensorProductModule The canonical A-linear isomorphism L ⊗ M ≅ B ⊗ M for any K-module M line 242 source
Source documentation
The canonical A-linear isomorphism L ⊗ M ≅ B ⊗ M for any K-module M.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, IsIntegralClosure, Algebra.IsAlgebraic, AddCommGroup, Module, LinearEquiv, RingHom.id, TensorProduct
Proof uses: LinearEquiv.restrictScalars, IsLocalization.moduleTensorEquiv, nonZeroDivisors, LinearEquiv.trans, IsDedekindDomain.LinearEquivTensorProduct, TensorProduct.comm, TensorProduct.congr, LinearEquiv.refl, TensorProduct.assoc, IsLocalization.moduleLid
64 instances, coercions and auxiliary constants left out.
```
noncomputable def linearEquivTensorProductModule : L ⊗[K] M ≃ₗ[A] B ⊗[A] M :=
…
```
def IsDedekindDomain.linearEquivTensorProductModuleLeft The canonical B-linear isomorphism L ⊗ M ≅ B ⊗ M for any K-module M line 256 source
Source documentation
The canonical B-linear isomorphism L ⊗ M ≅ B ⊗ M for any K-module M.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, IsIntegralClosure, Algebra.IsAlgebraic, AddCommGroup, Module, LinearEquiv, RingHom.id, TensorProduct
Proof uses: IsLocalization.leftModuleTensorEquiv, nonZeroDivisors, LinearEquiv.symm, LinearEquiv.trans, LinearEquiv.restrictScalars, IsDedekindDomain.LinearEquivTensorProduct, TensorProduct.comm, LinearEquiv.mk, LinearMap.mk, LinearMap.toAddHom, LinearEquiv.invFun, TensorProduct.AlgebraTensorModule.congr, LinearEquiv.refl, TensorProduct.AlgebraTensorModule.assoc, IsLocalization.moduleLid
75 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
noncomputable def linearEquivTensorProductModuleLeft : L ⊗[K] M ≃ₗ[B] B ⊗[A] M :=
…
```
lemma IsDedekindDomain.linearEquivTensorProductModuleLeft_restrictScalars line 277 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, IsIntegralClosure, Algebra.IsAlgebraic, AddCommGroup, Module, Eq, LinearEquiv, RingHom.id, TensorProduct, LinearEquiv.restrictScalars, IsDedekindDomain.linearEquivTensorProductModuleLeft, IsDedekindDomain.linearEquivTensorProductModule
Proof uses: Eq.refl
72 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.linearEquivTensorProductModule_symm_tmul line 282 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, IsIntegralClosure, Algebra.IsAlgebraic, AddCommGroup, Module, Eq, TensorProduct, LinearEquiv, RingHom.id, LinearEquiv.symm, IsDedekindDomain.linearEquivTensorProductModule, TensorProduct.tmul, RingHom, Algebra.algebraMap
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, LinearEquiv.trans, TensorProduct.assoc, TensorProduct.congr, TensorProduct.comm, LinearEquiv.restrictScalars, IsDedekindDomain.LinearEquivTensorProduct, LinearEquiv.refl, IsLocalization.moduleTensorEquiv, nonZeroDivisors, IsLocalization.moduleLid, OfNat.ofNat, LinearEquiv.restrictScalars_symm_apply, IsDedekindDomain.LinearEquivTensorProduct_symm_one_tmul, eq_self
79 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.linearEquivTensorProductModule_tmul line 287 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, IsIntegralClosure, Algebra.IsAlgebraic, AddCommGroup, Module, Eq, TensorProduct, LinearEquiv, RingHom.id, IsDedekindDomain.linearEquivTensorProductModule, TensorProduct.tmul, RingHom, Algebra.algebraMap
Proof uses: Eq.mpr, LinearEquiv.symm, id, congrArg, Eq.symm, propext, LinearEquiv.eq_symm_apply, IsDedekindDomain.linearEquivTensorProductModule_symm_tmul, Eq.refl
65 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.linearEquivTensorProductModuleLeft_symm_tmul line 291 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, IsIntegralClosure, Algebra.IsAlgebraic, AddCommGroup, Module, Eq, TensorProduct, LinearEquiv, RingHom.id, LinearEquiv.symm, IsDedekindDomain.linearEquivTensorProductModuleLeft, TensorProduct.tmul, RingHom, Algebra.algebraMap
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, LinearEquiv.trans, TensorProduct.AlgebraTensorModule.assoc, TensorProduct.AlgebraTensorModule.congr, LinearEquiv.mk, LinearMap.mk, LinearMap.toAddHom, TensorProduct.comm, LinearEquiv.restrictScalars, IsDedekindDomain.LinearEquivTensorProduct, AddHom, AddHom.toFun, HSMul.hSMul, id, Eq.refl, LinearMap and 13 more
100 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.linearEquivTensorProductModuleLeft_tmul line 295 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Field, IsFractionRing, IsDedekindDomain, IsScalarTower, IsIntegralClosure, Algebra.IsAlgebraic, AddCommGroup, Module, Eq, TensorProduct, LinearEquiv, RingHom.id, IsDedekindDomain.linearEquivTensorProductModuleLeft, TensorProduct.tmul, RingHom, Algebra.algebraMap
Proof uses: Eq.mpr, LinearEquiv.symm, id, congrArg, Eq.symm, propext, LinearEquiv.eq_symm_apply, IsDedekindDomain.linearEquivTensorProductModuleLeft_symm_tmul, Eq.refl
67 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma _root_.IsIntegralClosure.isLocalizedModule line 307 source