LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitPadicContinuousSMul
The actual principal-unit p-adic action is continuous in the valuation topology.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u
variable {K : Type u} [Field K] [Valued K (WithZero (Multiplicative ℤ))]
variable [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete
(Valued.v : _root_.Valuation K (WithZero (Multiplicative ℤ)))]
open CompleteDVF.higherPrincipalUnitGroupLean source · statement
theorem principalUnitPadicContinuousSMul (p : ℕ) [Fact p.Prime]
[hres : CharP (completeDVFOfWithZeroValuation
(Valued.v : _root_.Valuation K (WithZero (Multiplicative ℤ)))).residueField p] :
@ContinuousSMul ℤ_[p]
(Additive (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation
(Valued.v : _root_.Valuation K (WithZero (Multiplicative ℤ)))) 1))
(principalUnitPadicModuleOfResidueChar (completeDVFOfWithZeroValuation
(Valued.v : _root_.Valuation K (WithZero (Multiplicative ℤ)))) p).toSMul
inferInstance inferInstance