Documentation
Atlas
.
NumberTheoryI
.
code
.
Lemma247
Search
return to top
source
Imports
Init
Mathlib.LinearAlgebra.Matrix.Gershgorin
Mathlib.NumberTheory.NumberField.Units.Regulator
Imported by
lemma_24_7
source
theorem
lemma_24_7
{
K
:
Type
u_1}
[
Field
K
]
[
NumberField
K
]
(
u
:
NumberField.InfinitePlace
K
→
(
NumberField.RingOfIntegers
K
)
ˣ
)
(
hu
:
∀ (
v
w
:
NumberField.InfinitePlace
K
),
w
≠
v
→
w
(
(
algebraMap
(
NumberField.RingOfIntegers
K
)
K
)
↑
(
u
v
)
)
<
1
)
:
(
Subgroup.closure
(
Set.range
u
)
)
.
FiniteIndex