ClassFieldTheory.IsUnramifiedOutsideModulus
A number-field extension is unramified away from the finite primes and real places occurring in a ray modulus. Only the support of the finite part is used; this predicate does not bound conductor exponents.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory
universe u vLean source · statement
def IsUnramifiedOutsideModulus
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]
(m : RayClassModulus K) : Prop