TameAbhyankar.FieldNormCommon.subgroupValueSubgroup_fieldNormSubgroup_le_lcm_towers
The value image of the common-top field-norm subgroup lies in the lcm value-step subgroup generated by the two lower valued field-norm residue degrees.
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace TameAbhyankar
open LocalFieldTheory LocalFieldTheory.DiscreteValuationField
namespace FieldNormCommon
section TwoLowerTowers
variable {K L L' M : Type _}
variable [Field K] [Field L] [Field L'] [Field M]
variable [Algebra K L] [Algebra K L']
variable [Algebra K M]
variable [Algebra L M] [Algebra L' M]
variable [IsScalarTower K L M] [IsScalarTower K L' M]
variable [Module.Free L M] [Module.Free L' M]Lean source · statement
theorem subgroupValueSubgroup_fieldNormSubgroup_le_lcm_towers
(vK : MultiplicativeIntegerValuation Kˣ)
(vL : MultiplicativeIntegerValuation Lˣ)
(vL' : MultiplicativeIntegerValuation L'ˣ)
(residueDegree residueDegree' : ℕ)
(hformula :
∀ x : Lˣ, vK.val (normUnits K L x) =
(residueDegree : ℤ) * vL.val x)
(hformula' :
∀ x : L'ˣ, vK.val (normUnits K L' x) =
(residueDegree' : ℤ) * vL'.val x) :
vK.subgroupValueSubgroup (fieldNormSubgroup K M) ≤
integerMultipleSubgroup
((((residueDegree : ℤ).lcm (residueDegree' : ℤ) : ℕ) : ℤ))