Theorem Ideal.finrank_prime_pow_ramificationIdx

Modification history

2024-03-27 11:32

Mathlib/NumberTheory/RamificationInertia.lean

feat(DedekindDomain.Ideal): remove Domain assumption from DedekindDomain (#11527) …

Modified Ideal.finrank_prime_pow_ramificationIdx View on Github →

2023-06-08 06:34

Mathlib/NumberTheory/RamificationInertia.lean

feat: port NumberTheory.RamificationInertia (#4795)

Added Ideal.finrank_prime_pow_ramificationIdx View on Github →