Commit 2023-06-21 21:04 ce12efa0

View on Github →

feat: port RingTheory.Valuation.RamificationGroup (#5351)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Valuation/RamificationGroup.lean

added def ValuationSubring.decompositionSubgroup

added def ValuationSubring.inertiaSubgroup

added def ValuationSubring.subMulAction