ClassFieldTheory.lowerRamificationGroup_antitone
A larger lower index gives a smaller ramification subgroup.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTheory
universe u vLean source · statement
theorem lowerRamificationGroup_antitone
(K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
(A : ValuationSubring L) :
Antitone (lowerRamificationGroup K A)