Commit 2024-11-07 20:49 66e27ece

View on Github →

feat: the completion of a field at non-preferential absolute values (#18144) This PR contains the completion of a field at non-preferential absolute values.

Estimated changes

Modified Mathlib/Algebra/Ring/WithAbs.lean

added theorem AbsoluteValue.Completion.extensionEmbedding_dist_eq_of_comp

added theorem AbsoluteValue.Completion.extensionEmbedding_of_comp_coe

added theorem AbsoluteValue.Completion.isClosedEmbedding_extensionEmbedding_of_comp

added theorem AbsoluteValue.Completion.isometry_extensionEmbedding_of_comp

added theorem AbsoluteValue.Completion.locallyCompactSpace

added theorem WithAbs.isUniformInducing_of_comp

added theorem WithAbs.isometry_of_comp

added theorem WithAbs.pseudoMetricSpace_induced_of_comp

added theorem WithAbs.uniformSpace_comap_eq_of_comp

Modified Mathlib/Topology/Algebra/UniformRing.lean

added theorem UniformSpace.Completion.extensionHom_coe