ValuationTheory.DiscreteValuationField.Valuation.continuous_algebraMap_of_hasExtension
An extension of discrete valuations makes the algebra map continuous for the actual topologies induced by the two valuations.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationTheory.DiscreteValuationField.Valuation
variable {K L : Type*} [Field K] [Field L] [Algebra K L]Lean source · statement
theorem continuous_algebraMap_of_hasExtension
(vK : _root_.Valuation K (WithZero (Multiplicative ℤ)))
(vL : _root_.Valuation L (WithZero (Multiplicative ℤ)))
[vK.IsRankOneDiscrete] [vL.IsRankOneDiscrete] [vK.HasExtension vL] :
@Continuous K L (Valued.mk' vK).toUniformSpace.toTopologicalSpace
(Valued.mk' vL).toUniformSpace.toTopologicalSpace (algebraMap K L)