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

37 declarations, 0 contain sorry, 0 declared as axioms

Extensions of complex embeddings and infinite places of a number field

This file defines objects and classes for extensions of complex embeddings and extensions of infinite places. The relationship between the two is not one-to-one. If L / K are fields, w is an infinite place of L that extends the infinite place v over K, then there are four possibilities for the relationship between their respective associated complex embeddings w.embedding and v.embedding:

v is real, w is complex (w is a ramified extension of v), and both w.embedding and conjugate w.embedding extend v.embedding.
v and w are both real (i.e., w is an unramified real extension of v) and w.embedding extends v.embedding.
v and w are both complex (w is an unramified complex extension of v), and w.embedding extends v.embedding.
v and w are both complex, and conjugate w.embedding extends v.embedding.

Main definitions

ComplexEmbedding.IsExtension f g : predicate asserting that g : L →+* ℂ extends f : L →+* ℂ.
ComplexEmbedding.IsMixedExtension f g : predicate asserting that g : L →+* ℂ extends f : L →+* ℂ and g is complex while f is real.
ComplexEmbedding.IsUnmixedExtension f g : predicate asserting g : L →+* ℂ extends f : L →+* ℂ and that g is real if and only if f is real.
InfinitePlace.Extension L v : the type of infinite places of L extending v : InfinitePlace K .
InfinitePlace.RamifiedExtension L v : the type of infinite places of L that are ramified extensions of v : InfinitePlace K.
InfinitePlace.UnramifiedExtension L v : the type of infinite places of L that are unramified extensions of v : InfinitePlace K.
InfinitePlace.Extension.IsLift L v w: class encoding the property that w.embedding extends v.embedding.
InfinitePlace.Extension.IsConjugateLift L v w : class encoding the property that conjugate w.embedding extends v.embedding.

Imports (1)

Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Imported by 2 files

abbrev NumberField.ComplexEmbedding.IsExtension If L/K and f : K →+* ℂ, g : L →+* ℂ, then we say g is an extension of f if g restricted to K is f line 60 source
Source documentation
If L/K and f : K →+* ℂ, g : L →+* ℂ, then we say g is an extension of f if g restricted to K is f.
This is the complex embedding analogue of InfinitePlace.Extension.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, RingHom, Complex
Proof uses: Eq, RingHom.comp, Algebra.algebraMap
10 instances, coercions and auxiliary constants left out.
```
abbrev IsExtension := g.comp (algebraMap K L) = f
…
```
theorem NumberField.ComplexEmbedding.IsExtension.not_isExtension_conjugate line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, RingHom, Complex, NumberField.ComplexEmbedding.IsExtension, Not, NumberField.ComplexEmbedding.IsReal, NumberField.ComplexEmbedding.conjugate
Proof uses: of_eq_true, Eq.trans, Exists, Eq, starRingEnd, True, congrArg, RingHom.comp, Algebra.algebraMap, forall_congr, congrFun', id, Eq.mp, eq_true
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem NumberField.ComplexEmbedding.IsExtension.ne line 69 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, RingHom, Complex, NumberField.ComplexEmbedding.IsExtension, Not, Ne
Proof uses: Eq.mpr, Exists, Eq, id, Eq.trans, congrArg, Algebra.algebraMap, Eq.mp, RingHom.comp, congrFun', Eq.symm, Exists.intro, Aesop.BuiltinRules.not_intro, False.elim, False, True, eq_self, not_true_eq_false
16 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
abbrev NumberField.ComplexEmbedding.IsMixedExtension If L/K and f : K →+* ℂ, g : L →+* ℂ, then g is a mixed extension of f if the image of f is real while the image of g is complex line 82 source
Source documentation
If L/K and f : K →+* ℂ, g : L →+* ℂ, then g is a mixed extension of f if the image of f is real while the image of g is complex.
This is the complex embedding analogue of InfinitePlace.RamifiedExtension.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, RingHom, Complex
Proof uses: And, NumberField.ComplexEmbedding.IsExtension, NumberField.ComplexEmbedding.IsReal, Not
10 instances, coercions and auxiliary constants left out.
```
abbrev IsMixedExtension :=
…
```
theorem NumberField.ComplexEmbedding.not_isReal_of_not_isReal line 85 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, RingHom, Complex, NumberField.ComplexEmbedding.IsExtension, Not, NumberField.ComplexEmbedding.IsReal
Proof uses: mt, RingHom.comp, Algebra.algebraMap, NumberField.ComplexEmbedding.IsReal.comp, Eq.rec, Eq, Eq.symm
10 instances, coercions and auxiliary constants left out.
theorem NumberField.ComplexEmbedding.IsMixedExtension.isExtension line 92 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, RingHom, Complex, NumberField.ComplexEmbedding.IsMixedExtension, NumberField.ComplexEmbedding.IsExtension
Proof uses: And.left, And, NumberField.ComplexEmbedding.IsReal, Not
10 instances, coercions and auxiliary constants left out.
theorem NumberField.ComplexEmbedding.IsMixedExtension.isReal line 95 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, RingHom, Complex, NumberField.ComplexEmbedding.IsMixedExtension, NumberField.ComplexEmbedding.IsReal
Proof uses: And.left, Not, And.right, NumberField.ComplexEmbedding.IsExtension, And
10 instances, coercions and auxiliary constants left out.
theorem NumberField.ComplexEmbedding.IsMixedExtension.not_isReal line 98 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, RingHom, Complex, NumberField.ComplexEmbedding.IsMixedExtension, Not, NumberField.ComplexEmbedding.IsReal
Proof uses: And.right, NumberField.ComplexEmbedding.IsExtension, And
10 instances, coercions and auxiliary constants left out.
abbrev NumberField.ComplexEmbedding.IsUnmixedExtension If L/K and f : K →+* ℂ, g : L →+* ℂ, then g is an unmixed extension of f if g is an extension of f but is not a mixed extension line 110 source
Source documentation
If L/K and f : K →+* ℂ, g : L →+* ℂ, then g is an unmixed extension of f if g is an extension of f but is not a mixed extension. In other words, the image of f is real if and only if the image of g is real.
This is the complex embedding analogue of InfinitePlace.UnramifiedExtension.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, RingHom, Complex
Proof uses: And, NumberField.ComplexEmbedding.IsExtension, Not, NumberField.ComplexEmbedding.IsMixedExtension
10 instances, coercions and auxiliary constants left out.
```
abbrev IsUnmixedExtension := IsExtension f g ∧ ¬IsMixedExtension f g
…
```
Mentions: NumberField.ComplexEmbedding.IsExtension, NumberField.ComplexEmbedding.IsMixedExtension
theorem NumberField.ComplexEmbedding.IsUnmixedExtension.isReal_of_isReal line 113 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, RingHom, Complex, NumberField.ComplexEmbedding.IsUnmixedExtension, NumberField.ComplexEmbedding.IsReal
Proof uses: And.right, NumberField.ComplexEmbedding.IsExtension, Eq.mp, And, congrArg, Not, NumberField.ComplexEmbedding.IsMixedExtension, Eq.trans, implies_congr, Eq.refl, And.left
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def NumberField.ComplexEmbedding.isExtensionEquivSum The extensions g : L →+* ℂ of f : K →+* ℂ are the direct sum of the mixed and the unmixed extensions line 124 source
Source documentation
The extensions g : L →+* ℂ of f : K →+* ℂ are the direct sum of the mixed and the unmixed extensions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, RingHom, Complex, Equiv, Subtype, NumberField.ComplexEmbedding.IsExtension, Sum, NumberField.ComplexEmbedding.IsMixedExtension, NumberField.ComplexEmbedding.IsUnmixedExtension
Proof uses: Equiv.trans, And, NumberField.ComplexEmbedding.IsReal, Not, Equiv.symm, Equiv.sumCompl, Classical.propDecidable, Equiv.sumCongr, Equiv.subtypeSubtypeEquivSubtypeInter, Equiv.subtypeEquiv, Equiv.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def isExtensionEquivSum (f : K →+* ℂ) :
    { g : L →+* ℂ // IsExtension f g } ≃
      { g : L →+* ℂ // IsMixedExtension f g } ⊕ { g : L →+* ℂ // IsUnmixedExtension f g } :=
…
```
Mentions: NumberField.ComplexEmbedding.IsExtension, NumberField.ComplexEmbedding.IsMixedExtension, NumberField.ComplexEmbedding.IsUnmixedExtension
abbrev NumberField.InfinitePlace.Extension Documented declaration: Extension line 151 source
Source documentation
If L / K are fields and v is an infinite place of K, then we say an infinite place w of L extends v if w can be constructed from a complex embedding L →+* ℂ whose restriction to K is an associated complex embedding K →+* ℂ of v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace
Proof uses: Subtype, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap
6 instances, coercions and auxiliary constants left out.
```
abbrev Extension (v : InfinitePlace K) := { w : InfinitePlace L // w.comap (algebraMap K L) = v }
…
```
abbrev NumberField.InfinitePlace.toExtension Any infinite place w of L is an extension of its restriction to K line 155 source
Source documentation
Any infinite place w of L is an extension of its restriction to K.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField.InfinitePlace, Algebra, NumberField.InfinitePlace.Extension, NumberField.InfinitePlace.comap, Algebra.algebraMap
Proof uses: Subtype.mk, Eq
7 instances, coercions and auxiliary constants left out.
```
abbrev toExtension : (w.comap (algebraMap K L)).Extension L := ⟨w, rfl⟩
```
Mentions: NumberField.InfinitePlace.Extension
theorem NumberField.InfinitePlace.coe_toExtension line 157 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.toExtension
Proof uses: rfl
8 instances, coercions and auxiliary constants left out.
theorem NumberField.InfinitePlace.Extension.isComplex_of_isComplex line 163 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField.InfinitePlace.Extension, NumberField.InfinitePlace.IsComplex, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap
Proof uses: Eq.mpr, Not, NumberField.ComplexEmbedding.IsReal, NumberField.InfinitePlace.embedding, id, congrArg, propext, NumberField.InfinitePlace.isComplex_iff, RingHom, Complex, NumberField.ComplexEmbedding.conjugate, NumberField.ComplexEmbedding.isReal_iff, RingHom.ext_iff, Exists, Classical.not_forall, Eq.mp, Exists.intro, NumberField.InfinitePlace.mk, RingHom.comp, Or and 24 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem NumberField.InfinitePlace.Extension.isReal_base line 173 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField.InfinitePlace.Extension, NumberField.InfinitePlace.IsReal, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap
Proof uses: Eq.mpr, Not, NumberField.InfinitePlace.IsComplex, id, mt, NumberField.InfinitePlace.Extension.isComplex_of_isComplex, Eq.mp
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem NumberField.InfinitePlace.Extension.mk_embedding line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField.InfinitePlace.Extension, Eq, NumberField.InfinitePlace.mk, RingHom.comp, Complex, NumberField.InfinitePlace.embedding, NumberField.InfinitePlace.comap, Algebra.algebraMap
Proof uses: Eq.mpr, id, congrArg, Eq.symm, NumberField.InfinitePlace.comap_mk, NumberField.InfinitePlace.mk_embedding, Subtype.property, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem NumberField.InfinitePlace.Extension.isExtension_or_isExtension_conjugate line 181 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField.InfinitePlace.Extension, Or, NumberField.ComplexEmbedding.IsExtension, NumberField.InfinitePlace.embedding, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.ComplexEmbedding.conjugate
Proof uses: RingHom, Complex, NumberField.InfinitePlace.mk, RingHom.comp, NumberField.InfinitePlace.embedding_mk_eq, Or.inl, Eq.mpr, Eq.refl, Eq.rec, congrArg, NumberField.InfinitePlace.Extension.mk_embedding, Or.inr
11 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem NumberField.InfinitePlace.Extension.isExtension_conjugate_of_not_isExtension line 189 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField.InfinitePlace.Extension, Not, NumberField.ComplexEmbedding.IsExtension, NumberField.InfinitePlace.embedding, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.ComplexEmbedding.conjugate
Proof uses: Or.resolve_left, NumberField.InfinitePlace.Extension.isExtension_or_isExtension_conjugate
8 instances, coercions and auxiliary constants left out.
class NumberField.InfinitePlace.Extension.IsLift If w is an infinite place of L lying above the infinite place v of K, then there are two possibilities: - w.embedding extends v.embedding line 205 source
Source documentation
If w is an infinite place of L lying above the infinite place v of K, then there are two possibilities:
- w.embedding extends v.embedding.
- conjugate w.embedding extends v.embedding.
IsLift w encodes the first case.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField.InfinitePlace.Extension
3 instances, coercions and auxiliary constants left out.
```
class IsLift where
…
```
theorem NumberField.InfinitePlace.Extension.IsLift.isExtension line 208 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField.InfinitePlace.Extension, NumberField.InfinitePlace.Extension.IsLift, NumberField.ComplexEmbedding.IsExtension, NumberField.InfinitePlace.embedding, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap
Proof uses: NumberField.InfinitePlace.Extension.IsLift.isExtension'
7 instances, coercions and auxiliary constants left out.
class NumberField.InfinitePlace.Extension.IsConjugateLift If w is an infinite place of L lying above the infinite place v of K, then there are two possibilities: - w.embedding extends v.embedding line 219 source
Source documentation
If w is an infinite place of L lying above the infinite place v of K, then there are two possibilities:
- w.embedding extends v.embedding.
- conjugate w.embedding extends v.embedding.
IsConjugateLift w encodes the second case.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField.InfinitePlace.Extension
3 instances, coercions and auxiliary constants left out.
```
class IsConjugateLift where
…
```
theorem NumberField.InfinitePlace.Extension.IsConjugateLift.isExtension line 222 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField.InfinitePlace.Extension, NumberField.InfinitePlace.Extension.IsConjugateLift, NumberField.ComplexEmbedding.IsExtension, NumberField.InfinitePlace.embedding, NumberField.ComplexEmbedding.conjugate, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap
Proof uses: NumberField.InfinitePlace.Extension.IsConjugateLift.isExtension'
7 instances, coercions and auxiliary constants left out.
theorem NumberField.InfinitePlace.Extension.isLift_or_isConjugateLift line 225 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField.InfinitePlace.Extension, Or, NumberField.InfinitePlace.Extension.IsLift, NumberField.InfinitePlace.Extension.IsConjugateLift
Proof uses: NumberField.ComplexEmbedding.IsExtension, NumberField.InfinitePlace.embedding, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.ComplexEmbedding.conjugate, NumberField.InfinitePlace.Extension.isExtension_or_isExtension_conjugate, Or.inl, NumberField.InfinitePlace.Extension.IsLift.mk, Or.inr, NumberField.InfinitePlace.Extension.IsConjugateLift.mk, Eq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
abbrev NumberField.InfinitePlace.RamifiedExtension For a given infinite place v of K, RamifiedExtension L v are all the infinite places of L / K that extend v and are ramified over K line 237 source
Source documentation
For a given infinite place v of K, RamifiedExtension L v are all the infinite places of L / K that extend v and are ramified over K.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace
Proof uses: Subtype, And, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.IsRamified
6 instances, coercions and auxiliary constants left out.
```
abbrev RamifiedExtension (v : InfinitePlace K) :=
…
```
abbrev NumberField.InfinitePlace.UnramifiedExtension For a given infinite place v of K, UnramifiedExtension L v are all the infinite places of L / K that extend v and are unramified over K line 242 source
Source documentation
For a given infinite place v of K, UnramifiedExtension L v are all the infinite places of L / K that extend v and are unramified over K.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace
Proof uses: Subtype, And, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.IsUnramified
6 instances, coercions and auxiliary constants left out.
```
abbrev UnramifiedExtension (v : InfinitePlace K) :=
…
```
def NumberField.InfinitePlace.Extension.toRamifiedExtension Construct a v.RamifiedExtension L term from a w : v.Extension L such that w.1.IsRamified K line 249 source
Source documentation
Construct a v.RamifiedExtension L term from a w : v.Extension L such that w.1.IsRamified K.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField.InfinitePlace, Algebra, NumberField.InfinitePlace.Extension, NumberField.InfinitePlace.IsRamified, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.RamifiedExtension
Proof uses: Subtype.mk, And
9 instances, coercions and auxiliary constants left out.
```
def Extension.toRamifiedExtension {w : v.Extension L} (h : w.1.IsRamified K) :
    v.RamifiedExtension L := ⟨w.1, ⟨w.2, h⟩⟩
```
def NumberField.InfinitePlace.Extension.toUnramifiedExtension Construct a v.UnramifiedExtension L term from a w : v.Extension L such that w.1.IsUnramified K line 254 source
Source documentation
Construct a v.UnramifiedExtension L term from a w : v.Extension L such that w.1.IsUnramified K.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField.InfinitePlace, Algebra, NumberField.InfinitePlace.Extension, NumberField.InfinitePlace.IsUnramified, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.UnramifiedExtension
Proof uses: Subtype.mk, And
9 instances, coercions and auxiliary constants left out.
```
def Extension.toUnramifiedExtension {w : v.Extension L} (h : w.1.IsUnramified K) :
    v.UnramifiedExtension L := ⟨w.1, ⟨w.2, h⟩⟩
…
```
theorem NumberField.InfinitePlace.RamifiedExtension.comap_eq line 259 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField.InfinitePlace, Algebra, NumberField.InfinitePlace.RamifiedExtension, Eq, NumberField.InfinitePlace.comap, And, Algebra.algebraMap, NumberField.InfinitePlace.IsRamified
Proof uses: And.left, Subtype.property
8 instances, coercions and auxiliary constants left out.
theorem NumberField.InfinitePlace.RamifiedExtension.isRamified line 261 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField.InfinitePlace, Algebra, NumberField.InfinitePlace.RamifiedExtension, NumberField.InfinitePlace.IsRamified, And, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap
Proof uses: And.right, Subtype.property
8 instances, coercions and auxiliary constants left out.
theorem NumberField.InfinitePlace.RamifiedExtension.isReal_comap line 263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField.InfinitePlace, Algebra, NumberField.InfinitePlace.RamifiedExtension, NumberField.InfinitePlace.IsReal, NumberField.InfinitePlace.comap, And, Eq, Algebra.algebraMap, NumberField.InfinitePlace.IsRamified
Proof uses: And.right, NumberField.InfinitePlace.IsComplex, Iff.mp, NumberField.InfinitePlace.isRamified_iff, NumberField.InfinitePlace.RamifiedExtension.isRamified
8 instances, coercions and auxiliary constants left out.
instance NumberField.InfinitePlace.RamifiedExtension.(instance at line 266) line 266 source
theorem NumberField.InfinitePlace.RamifiedExtension.isReal line 269 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField.InfinitePlace, Algebra, NumberField.InfinitePlace.RamifiedExtension, NumberField.InfinitePlace.IsReal
Proof uses: Eq.rec, NumberField.InfinitePlace.comap, And, Eq, Algebra.algebraMap, NumberField.InfinitePlace.IsRamified, NumberField.InfinitePlace.RamifiedExtension.isReal_comap, NumberField.InfinitePlace.RamifiedExtension.comap_eq
7 instances, coercions and auxiliary constants left out.
theorem NumberField.InfinitePlace.RamifiedExtension.isComplex line 272 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField.InfinitePlace, Algebra, NumberField.InfinitePlace.RamifiedExtension, NumberField.InfinitePlace.IsComplex, And, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.IsRamified
Proof uses: And.left, NumberField.InfinitePlace.IsReal, Iff.mp, NumberField.InfinitePlace.isRamified_iff, NumberField.InfinitePlace.RamifiedExtension.isRamified
8 instances, coercions and auxiliary constants left out.
theorem NumberField.InfinitePlace.UnramifiedExtension.comap_eq line 280 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField.InfinitePlace, Algebra, NumberField.InfinitePlace.UnramifiedExtension, Eq, NumberField.InfinitePlace.comap, And, Algebra.algebraMap, NumberField.InfinitePlace.IsUnramified
Proof uses: And.left, Subtype.property
8 instances, coercions and auxiliary constants left out.
theorem NumberField.InfinitePlace.UnramifiedExtension.isUnramified line 282 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField.InfinitePlace, Algebra, NumberField.InfinitePlace.UnramifiedExtension, NumberField.InfinitePlace.IsUnramified, And, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap
Proof uses: And.right, Subtype.property
8 instances, coercions and auxiliary constants left out.
instance NumberField.InfinitePlace.UnramifiedExtension.(instance at line 284) line 284 source