Lemmas.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

43 declarations, 0 contain sorry, 0 declared as axioms

Miscellaneous lemmas for the Deformations folder

A collection of small auxiliary lemmas used in the deformation-theory files: existence of open maximal ideals in linearly topologized rings, continuous group-homomorphism / matrix-coefficient lifts, etc.

Imports (9)

Imported by 6 files

lemma IsLinearTopology.exists_ideal_isMaximal_and_isOpen line 28 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, IsTopologicalRing, IsLinearTopology, Nontrivial, T0Space, Exists, Ideal, And, Ideal.IsMaximal, IsOpen
Proof uses: LE.le, Set, Compl.compl, Singleton.singleton, OfNat.ofNat, Iff.mp, Membership.mem, Filter, nhds, Filter.HasBasis.mem_iff, IsLinearTopology.hasBasis_open_ideal, IsOpen.mem_nhds, IsClosed.isOpen_compl, isClosed_singleton, of_eq_true, Eq.trans, Not, True, False, congrArg and 12 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Units.mapₜ The continuous group homomorphism on units induced by a ContinuousMonoidHom line 39 source
Source documentation
The continuous group homomorphism on units induced by a ContinuousMonoidHom.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monoid, TopologicalSpace, ContinuousMonoidHom, Units
Proof uses: ContinuousMonoidHom.mk, Units.map
10 instances, coercions and auxiliary constants left out.
```
def Units.mapₜ {M N : Type*} [Monoid M] [Monoid N] [TopologicalSpace M] [TopologicalSpace N]
    (f : M →ₜ* N) : Mˣ →ₜ* Nˣ :=
…
```
def ContinuousAlgHom.mapMatrix The ContinuousAlgHom between spaces of square matrices induced by an ContinuousAlgHom between their coefficients line 48 source
Source documentation
The ContinuousAlgHom between spaces of square matrices induced by an ContinuousAlgHom between their coefficients. This is Matrix.map as an ContinuousAlgHom.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommSemiring, Semiring, TopologicalSpace, Algebra, ContinuousAlgHom, Fintype, DecidableEq, Matrix
Proof uses: ContinuousAlgHom.mk, AlgHom.mapMatrix
8 instances, coercions and auxiliary constants left out.
```
def ContinuousAlgHom.mapMatrix
    {R A B n : Type*} [CommSemiring R] [Semiring A] [Semiring B] [TopologicalSpace A]
    [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B)
    [Fintype n] [DecidableEq n] :
    Matrix n n A →A[R] Matrix n n B :=
…
```
def ContinuousAlgHom.toContinuousMonoidHom Coerce a ContinuousAlgHom to ContinuousMonoidHom line 56 source
Source documentation
Coerce a ContinuousAlgHom to ContinuousMonoidHom.

no axioms what this means
Statement uses: CommSemiring, Semiring, TopologicalSpace, Algebra, ContinuousAlgHom, ContinuousMonoidHom
Proof uses: ContinuousMonoidHom.mk, AlgHom.toRingHom, ContinuousAlgHom.cont
5 instances, coercions and auxiliary constants left out.
```
def ContinuousAlgHom.toContinuousMonoidHom
    {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B] [TopologicalSpace A]
    [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) : A →ₜ* B :=
…
```
lemma ContinuousAlgHom.coe_toContinuousMonoidHom line 62 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommSemiring, Semiring, TopologicalSpace, Algebra, ContinuousAlgHom, Eq, ContinuousMonoidHom, ContinuousAlgHom.toContinuousMonoidHom
Proof uses: rfl
7 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
instance (instance at line 67) line 67 source
lemma MonoidHom.coe_smul line 74 source
standard axioms: Quot.sound, propext what this means
Statement uses: Monoid, MulDistribMulAction, MonoidHom, Eq, HSMul.hSMul
Proof uses: rfl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
instance (instance at line 79) line 79 source
lemma ContinuousMonoidHom.coe_smul line 87 source
standard axioms: Quot.sound, propext what this means
Statement uses: Monoid, MulDistribMulAction, TopologicalSpace, ContinuousConstSMul, ContinuousMonoidHom, Eq, HSMul.hSMul
Proof uses: rfl
17 instances, coercions and auxiliary constants left out.
instance (instance at line 93) line 93 source
instance IsTopologicalGroup.discreteUniformity line 98 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, TopologicalSpace, IsTopologicalGroup, DiscreteTopology, DiscreteUniformity, IsTopologicalGroup.rightUniformSpace
Proof uses: Eq.mpr, Membership.mem, SetRel, Filter, Prod, uniformity, SetRel.id, id, Eq, Exists.intro, Set, And, nhds, OfNat.ofNat, LE.le, Set.preimage, HMul.hMul, Prod.snd, Inv.inv, Prod.fst and 20 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma IsLocalRing.ResidueField.map_surjective line 105 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, RingHom, IsLocalHom, Function.Surjective, IsLocalRing.ResidueField, IsLocalRing.ResidueField.map
Proof uses: Ideal.Quotient.lift_surjective_of_surjective, IsLocalRing.maximalIdeal, RingHom.comp, HasQuotient.Quotient, Ideal, Ideal.Quotient.mk, Membership.mem, Function.Surjective.comp, Ideal.Quotient.mk_surjective
29 instances, coercions and auxiliary constants left out.
lemma RingHom.continuous_iff_isOpen_ker line 110 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Ring, Semiring, RingHom, DiscreteTopology, IsTopologicalAddGroup, Iff, Continuous, IsOpen, Ideal, RingHom.ker
Proof uses: AddMonoidHom.continuous_iff_isOpen_ker, RingHom.toAddMonoidHom
19 instances, coercions and auxiliary constants left out.
lemma continuousAt_discrete_rng line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, DiscreteTopology, Iff, ContinuousAt, Filter.Eventually, Eq, nhds
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Filter.Tendsto, Pure.pure, Filter, congrFun, nhds_discrete, iff_self
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
instance ContinuousAlgHom.isLocalHom_id line 122 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommSemiring, Semiring, Algebra, TopologicalSpace, IsLocalHom, ContinuousAlgHom, ContinuousAlgHom.id
Proof uses: Eq.mpr, RingHom, RingHom.id, propext, Iff.intro, IsUnit, IsLocalHom.mk
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ContinuousAlgHom.isLocalHom_toRingHom line 128 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommSemiring, Semiring, Algebra, TopologicalSpace, ContinuousAlgHom, Iff, IsLocalHom, RingHom, AlgHom.toRingHom
Proof uses: Iff.intro, IsUnit, IsLocalHom.mk
13 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
instance (instance at line 136) line 136 source
instance (instance at line 141) line 141 source
instance (instance at line 147) line 147 source
instance (instance at line 152) line 152 source
instance (instance at line 158) line 158 source
instance ContinuousAlgHom.isLocalHom_comp line 161 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommSemiring, Semiring, Algebra, TopologicalSpace, ContinuousAlgHom, IsLocalHom, ContinuousAlgHom.comp
Proof uses: Eq.mpr, RingHom, RingHom.comp, AlgHom.toRingHom, propext, Iff.intro, IsUnit, IsLocalHom.mk
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance (instance at line 171) line 171 source
instance (instance at line 175) line 175 source
def AlgebraicClosure.map line 181 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, RingHom, AlgebraicClosure
Proof uses: AlgHom.toRingHom, RingHom.toAlgebra, IsAlgClosed.lift
21 instances, coercions and auxiliary constants left out.
lemma AlgebraicClosure.map_algebraMap line 186 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, RingHom, Eq, AlgebraicClosure, AlgebraicClosure.map, Algebra.algebraMap
Proof uses: AlgHom.commutes, RingHom.toAlgebra, IsAlgClosed.lift
39 instances, coercions and auxiliary constants left out.
lemma IsModuleTopology.continuous_det line 192 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, IsTopologicalRing, AddCommGroup, Module, Module.End, IsModuleTopology, RingHom.id, Continuous, LinearMap, MonoidHom, LinearMap.det
Proof uses: dite, Exists, Finset, Nonempty, Module.Basis, Subtype, Membership.mem, Classical.propDecidable, Matrix, ContinuousAdd, IsModuleTopology.toContinuousAdd, ContinuousAlgEquiv, Eq, AlgEquiv, algEquivMatrix, ContinuousAlgEquiv.mk, IsModuleTopology.continuous_of_linearMap, AlgEquiv.toLinearMap, AlgEquiv.symm, Eq.mpr and 30 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
def Module.endSelf End_A(A) ≃ A line 213 source
Source documentation
End_A(A) ≃ A.

standard axioms: Quot.sound, propext what this means
Statement uses: CommSemiring, AlgEquiv, Module.End
Proof uses: AlgEquiv.ofLinearEquiv, LinearMap.ringLmapEquivSelf
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def Module.endSelf {A : Type*} [CommSemiring A] : Module.End A A ≃ₐ[A] A :=
…
```
def ContinuousMonoidHom.toHomUnits Given a ContinuousMonoidHom from a group to a monoid, we may lift it to map into the group of units of the monoid line 219 source
Source documentation
Given a ContinuousMonoidHom from a group to a monoid, we may lift it to map into the group of units of the monoid.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Monoid, TopologicalSpace, IsTopologicalGroup, ContinuousMonoidHom, Units
Proof uses: ContinuousMonoidHom.mk, MonoidHom.toHomUnits
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def ContinuousMonoidHom.toHomUnits {G M : Type*} [Group G] [Monoid M] [TopologicalSpace G]
    [IsTopologicalGroup G] [TopologicalSpace M] (f : G →ₜ* M) : G →ₜ* Mˣ :=
…
```
def Units.coeHomₜ Units.val as a ContinuousMonoidHom line 226 source
Source documentation
Units.val as a ContinuousMonoidHom.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monoid, TopologicalSpace, ContinuousMonoidHom, Units
Proof uses: ContinuousMonoidHom.mk, Units.coeHom, Units.continuous_val
4 instances, coercions and auxiliary constants left out.
```
def Units.coeHomₜ (M : Type*) [Monoid M] [TopologicalSpace M] : Mˣ →ₜ* M :=
…
```
instance (instance at line 229) line 229 source
def ContinuousAlgEquiv.ofIsModuleTopology We can upgrade an AlgEquiv between algebras with the module topology into a ContinuousAlgEquiv line 235 source
Source documentation
We can upgrade an AlgEquiv between algebras with the module topology into a ContinuousAlgEquiv.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommSemiring, Semiring, Algebra, TopologicalSpace, IsModuleTopology, AlgEquiv, ContinuousAlgEquiv
Proof uses: ContinuousAlgEquiv.mk
8 instances, coercions and auxiliary constants left out.
```
def ContinuousAlgEquiv.ofIsModuleTopology {R A B : Type*} [CommSemiring R] [Semiring A]
    [Semiring B] [Algebra R A] [Algebra R B] [TopologicalSpace A] [TopologicalSpace B]
    [TopologicalSpace R] [IsModuleTopology R A] [IsModuleTopology R B] (e : A ≃ₐ[R] B) :
    A ≃A[R] B where
…
```
lemma ContinuousMonoidHom.mk_toMonoidHom line 248 source
no axioms what this means
Statement uses: Monoid, TopologicalSpace, MonoidHom, Continuous, Eq, ContinuousMonoidHom, ContinuousMonoidHom.mk
Proof uses: rfl
14 instances, coercions and auxiliary constants left out.
lemma ContinuousMonoidHom.coe_mk line 252 source
no axioms what this means
Statement uses: Monoid, TopologicalSpace, MonoidHom, Continuous, Eq, ContinuousMonoidHom, ContinuousMonoidHom.mk
Proof uses: rfl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance (instance at line 255) line 255 source
instance (instance at line 269) line 269 source
lemma Subring.algebraMap_def line 279 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, Subring, Eq, RingHom, Subtype, Membership.mem, Algebra.algebraMap, Subring.subtype
Proof uses: rfl
24 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
instance (instance at line 282) line 282 source
instance (instance at line 286) line 286 source
instance (instance at line 290) line 290 source
instance IntermediateField.smulCommClass_of_normal line 297 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, IntermediateField, Monoid, MulSemiringAction, SMulCommClass, Normal, Subtype, Membership.mem
Proof uses: SMulCommClass.mk, Subtype.ext, HSMul.hSMul, SMulCommClass.smul_comm
86 instances, coercions and auxiliary constants left out.
instance ValuationSubring.smulCommClass line 303 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Semiring, ValuationSubring, Algebra, Monoid, MulSemiringAction, SMulCommClass, Subtype, Membership.mem
Proof uses: SMulCommClass.mk, SMulCommClass.smul_comm
47 instances, coercions and auxiliary constants left out.
instance Additive.instDistrbMulAction line 310 source
standard axioms: Quot.sound what this means
Statement uses: Monoid, MulDistribMulAction, DistribMulAction, Additive
Proof uses: DistribMulAction.mk, MulAction.mk, SemigroupAction.mk, SMul.mk, Equiv, Additive.ofMul, HSMul.hSMul, Additive.toMul, MulDistribMulAction.smul_one
13 instances, coercions and auxiliary constants left out.