Commit 2023-03-22 07:52 5d08b558

View on Github →

feat: port Topology/Algebra/UniformRing (#2789)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/UniformRing.lean

added theorem UniformSpace.Completion.Continuous.mul

added theorem UniformSpace.Completion.algebraMap_def

added def UniformSpace.Completion.coeRingHom

added theorem UniformSpace.Completion.coe_mul

added theorem UniformSpace.Completion.coe_one

added theorem UniformSpace.Completion.continuous_coeRingHom

added theorem UniformSpace.Completion.continuous_mul

added def UniformSpace.Completion.extensionHom

added def UniformSpace.Completion.mapRingHom

added theorem UniformSpace.Completion.map_smul_eq_mul_coe

added theorem UniformSpace.ring_sep_quot

added theorem UniformSpace.ring_sep_rel

added def UniformSpace.sepQuotEquivRingQuot