LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.map_padicIntToFieldOfMixedChar
The constructed p-adic integer maps commute with an extension of complete discrete valuations.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
variable {K L : Type*} [Field K] [Field L] [Algebra K L]Lean source · statement
theorem map_padicIntToFieldOfMixedChar
(vK : _root_.Valuation K (WithZero (Multiplicative ℤ)))
(vL : _root_.Valuation L (WithZero (Multiplicative ℤ)))
[ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete vK]
[ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete vL]
[vK.HasExtension vL]
(p : ℕ) [Fact p.Prime]
[CharP (IsLocalRing.ResidueField vK.valuationSubring) p]
[CharP (IsLocalRing.ResidueField vL.valuationSubring) p]
(a : ℤ_[p]) :
algebraMap K L (padicIntToFieldOfMixedChar vK p a) =
padicIntToFieldOfMixedChar vL p a