Module

RationalPrime.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.RationalPrime

2 declarations indexed from sourceView source ↗

Module documentation

This file identifies the height-one ideal of ℤ attached to a positive rational prime with its usual principal ideal.

Imports2

Imported by5

abbrev

AlgebraicNumberTheory.Ramification.rationalPrimeIdeal

Documentation

The height-one ideal of ℤ corresponding to a positive rational prime.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory.Ramification

Lean source · statement

abbrev rationalPrimeIdeal (p : Nat.Primes) : Ideal ℤ

theorem

AlgebraicNumberTheory.Ramification.rationalPrimeIdeal_eq_span

Documentation

The height-one ideal represented by a positive rational prime is its usual principal ideal.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory.Ramification

Lean source · statement

theorem rationalPrimeIdeal_eq_span (p : Nat.Primes) :
    rationalPrimeIdeal p = Ideal.span {(p.1 : ℤ)}