Documentation
Atlas
.
NumberTheoryI
.
code
.
Prop22_4_RayClassGroup
Search
return to top
source
Imports
Init
Atlas.NumberTheoryI.code.Cor227
Atlas.NumberTheoryI.code.GlobalCFT
Atlas.NumberTheoryI.code.RayClassFields
Imported by
proposition_22_4_equivalence
source
theorem
proposition_22_4_equivalence
{
K
:
Type
u_1}
[
Field
K
]
[
NumberField
K
]
:
Equivalence
RayClassField.CongruenceSubgroupPair.IsEquiv