ClassFieldTheory.realLowerRamificationGroup_nat
The real lower group at a natural index is the original lower group.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTheory
universe u vLean source · statement
theorem realLowerRamificationGroup_nat
(K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
(A : ValuationSubring L) (n : ℕ) :
realLowerRamificationGroup K A (n : ℝ) = lowerRamificationGroup K A n